X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.ml;h=36e9f99a64a710785976c200979d0764620bc849;hb=0e6ba9d1134a3bfe9fd4d5b4495faf0811a216df;hp=ab27f8a314b13e4b75cce13afbd272a7f9440475;hpb=c90dd454864f9383d7b05cd060e656fbe69b52bd;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index ab27f8a31..36e9f99a6 100644
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -139,7 +139,10 @@ let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 
 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
-  let metasenv = metasenv1 @ metasenv2 in
+  let metasenv = 
+    HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
+    (*metasenv1 @ metasenv2*)
+  in
   let subst, menv, ug =
     if not (is_simple_term t1) || not (is_simple_term t2) then (
       debug_print