Commit 719386bf authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

tptp: we will not support inclusions

Why3 library mechanism is not adapted for forward dependencies.
parent 77cdbd32
......@@ -665,10 +665,8 @@ let typecheck lib path ast =
let pr = create_prsymbol (id_fresh "contradiction") in
env, add_prop_decl uc Pgoal pr t_false
(* includes *)
| Include (_f,[],_loc) ->
assert false (* TODO: include *)
| Include (_,_,loc) ->
errorm ~loc "Formula selection is not supported"
errorm ~loc "Inclusion is not supported"
(* FIXME: localize the identifier *)
let uc = create_theory ~path (id_fresh "T") in
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment