all pullbacks are attempted in sequence, removed many unfold

[helm.git] / helm / software / components / tactics / paramodulation / founif.ml

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index 87550f76aa20c2eed4478e0271aa65900c118af2..c2df6371c410fa8da7d18b9b6d296c6a1b0d8bb2 100644 (file)
--- a/helm/software/components/tactics/paramodulation/founif.ml
+++ b/helm/software/components/tactics/paramodulation/founif.ml
@@ -225,6 +225,13 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph =
 ;;
 
 let unification m1 m2 c t1 t2 ug = 
+  let m1 =
+    if (m1 = m2 && m1 <> []) then assert false
+      (* (prerr_endline "eccoci 2"; []) *) else m1 in
+  (*   
+  prerr_endline (CicPp.ppterm t1);
+  prerr_endline (CicPp.ppterm t2);
+  prerr_endline "++++++++++"; *)
   try 
     unification_aux true m1 m2 c t1 t2 ug
   with exn ->