HExtlib.list_uniq (List.sort compare (aux a))
;;
+let collect_fv_from_formulae = function
+ | A.Disjunction _ -> assert false
+ | A.NegAtom a
+ | A.Atom a -> collect_fv_from_atom a
+;;
+
let rec convert_term = function
| A.Variable x -> mk_ident x
| A.Constant x -> mk_ident x
| A.Hypothesis ->
statements, f::context
| A.Negated_conjecture ->
+ if collect_fv_from_formulae f <> [] then
+ prerr_endline "CONTIENE FV";
let f =
PT.Binder
(`Forall,