rc
;;
-
(* returns the list of ids that should be factorized *)
let get_duplicate_step_in_wfo bag l p =
let ol = List.rev l in
let fix_metas_goal (id_to_eq,newmeta) goal =
let (proof, menv, ty) = goal in
- let to_be_relocated =
- HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty))
- in
+ let to_be_relocated = List.map (fun i ,_,_ -> i) menv in
let subst, menv, newmeta = relocate newmeta menv to_be_relocated in
let ty = Subst.apply_subst subst ty in
let proof =
ignore(Unix.system "gv /tmp/matita_paramod.eps");
;;
-let saturate_term (id_to_eq, maxmeta) metasenv context term =
+let saturate_term (id_to_eq, maxmeta) metasenv subst context term =
+ let maxmeta = max maxmeta (CicMkImplicit.new_meta metasenv subst) in
let head, metasenv, args, newmeta =
TermUtil.saturate_term maxmeta metasenv context term 0
in