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
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