Almost ready to implement coercion declaration for record fields. But how?

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index bf0e71bbd0db548a2f81aa48520c13c732c95fbf..2bf3600f289d4de84e76daa71a2f3197bd78c1bb 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -716,7 +716,6 @@ let topological_sort bag l =
   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
@@ -898,9 +897,7 @@ let relocate newmeta menv to_be_relocated =
 
 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 = 
@@ -1367,7 +1364,8 @@ let draw_proof bag names goal_proof proof id =
   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