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 c2df6371c410fa8da7d18b9b6d296c6a1b0d8bb2..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;;