Commit ec27f357 authored by Francois Bobot's avatar Francois Bobot

Encoding instantiate assert for term in fmla...

parent c51249bb
......@@ -308,7 +308,7 @@ and rewrite_fmla menv tvar vsvar f =
(* Pretty.print_ty u.vs_ty Pretty.print_ty t1.t_ty; *)
assert (u.vs_ty == t1.t_ty);
f_let t1 (cb u f2)
| _ -> f_map (fnT vsvar) (fnF vsvar) f
| _ -> f_map (fun _ -> assert false) (fnF vsvar) f
(* Generation of all the possible instantiation of a formula *)
let gen_tvar env ts =
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment