X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.ml;h=6a21bb173d1f76f8cc380b56b4bd34160beed287;hb=c92a4b4096c9633c27a6cb392d8027cad4c34144;hp=ccc73c351e3d8f422b33a90007f4f9db44095e07;hpb=356f9fafa095801f1be70ff495f0977ce96ed6bc;p=helm.git

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index ccc73c351..6a21bb173 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/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
@@ -488,4 +491,5 @@ let find_context_hypotheses env equalities_indexes =
   in
   res
 ;;
+
 let get_stats () = <:show<Inference.>> ;;