X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2FnCicParamod.ml;h=ef9852fcc359c24a7d322b213260595343ddf3ef;hb=b804ff9f8fba300ffaa54add291e0f6490b757ce;hp=16ae66e5da45f76259420625ebd2311247899987;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_paramodulation/nCicParamod.ml b/matita/components/ng_paramodulation/nCicParamod.ml
index 16ae66e5d..ef9852fcc 100644
--- a/matita/components/ng_paramodulation/nCicParamod.ml
+++ b/matita/components/ng_paramodulation/nCicParamod.ml
@@ -16,8 +16,9 @@ NCicBlob.set_default_eqP()
 NCicProof.set_default_sig()
 ;;
 
-let debug _ = ();;
+let noprint _ = ();;
 let print s = prerr_endline (Lazy.force s);; 
+let debug = noprint;; 
 
 module B(C : NCicBlob.NCicContext): Orderings.Blob 
   with type t = NCic.term and type input = NCic.term 
@@ -164,7 +165,6 @@ let is_equation metasenv subst context ty =
     | _ -> false
 ;;
 
-
 (*
 let demodulate rdb metasenv subst context s goal =
   (* let stamp = Unix.gettimeofday () in *)