huge commit in automation:

[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..5888019e4f78f584c047478a3a13d22b8177561e 100644 (file)
--- 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 =