X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Ffounif.ml;h=b635599515b75ba0d77fc7f6e7cbe793df66ee9a;hb=b8934a9598d747662139c74c751b8223bcc19d03;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..b63559951 100644
--- a/helm/software/components/tactics/paramodulation/founif.ml
+++ b/helm/software/components/tactics/paramodulation/founif.ml
@@ -206,9 +206,10 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   if Utils.debug_metas then
     ignore(check_for_duplicates menv "unification_aux prima di apply_subst");
   let menv = Subst.apply_subst_metasenv subst menv in
-  let _ = check_for_duplicates menv "unif_aux after" in
-    check_metasenv "unification_aux after 1" menv;
-    subst, menv, ug
+  if Utils.debug_metas then
+    (let _ = check_for_duplicates menv "unif_aux after" in
+    check_metasenv "unification_aux after 1" menv);
+  subst, menv, ug
 ;;
 
 exception MatchingFailure;;
@@ -225,6 +226,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 ->