X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.ml;h=a3894fd84cdbfa374ecc3e570ac8bbbb2fad57df;hb=430fb6e217b6ca61bfc38bb970c1bc57d5643b4c;hp=547a235590a7991ddc8144f94f0ade20984b7aa7;hpb=21933bca0834a45119f567b17b6f641113b881bb;p=helm.git

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 547a23559..a3894fd84 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -541,11 +541,11 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
           subst, menv
         with CicUtil.Meta_not_found m ->
           let names = names_of_context context in
-          debug_print
-            (lazy
+          (*debug_print
+            (lazy*) prerr_endline 
                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
                   (CicPp.pp t1 names) (CicPp.pp t2 names)
-                  (print_metasenv menv) (print_metasenv metasenv)));
+                  (print_metasenv menv) (print_metasenv metasenv));
           assert false
       )
     | _, C.Meta _ -> unif subst menv t s