X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=2bf3600f289d4de84e76daa71a2f3197bd78c1bb;hb=b0325c1fa8f59f8aaff2b6df59f3852338e82523;hp=bf0e71bbd0db548a2f81aa48520c13c732c95fbf;hpb=7cb22a7f8107a6cde0b77b7879e04f586a347102;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index bf0e71bbd..2bf3600f2 100644
--- 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