many checks guarded with if Utils.debug_metas

[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..b635599515b75ba0d77fc7f6e7cbe793df66ee9a 100644 (file)
--- 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 ->