X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Ffounif.ml;h=c2df6371c410fa8da7d18b9b6d296c6a1b0d8bb2;hb=0080faad4e730c227b6bbb2549407b23703b477a;hp=87550f76aa20c2eed4478e0271aa65900c118af2;hpb=d7f3ff62899afb162cb2825af91de72fe6d8dc85;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index 87550f76a..c2df6371c 100644
--- 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 ->