Subsumption_subst must be applied to the initial proof before passing

[helm.git] / components / tactics / paramodulation / inference.ml

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 36e9f99a64a710785976c200979d0764620bc849..6a21bb173d1f76f8cc380b56b4bd34160beed287 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -140,8 +140,8 @@ let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 
 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   let metasenv = 
-    HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
-    (*metasenv1 @ metasenv2*)
+    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 (