X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=5888019e4f78f584c047478a3a13d22b8177561e;hb=dcef667a444aa0f189225855c1433d26b65fb8b7;hp=bf0e71bbd0db548a2f81aa48520c13c732c95fbf;hpb=134014e54c374789b38b6c53945f63d21ddbacb0;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index bf0e71bbd..5888019e4 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -898,9 +898,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 =