From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Nov 2010 10:52:40 +0000 (+0000)
Subject: Debugging disabled
X-Git-Tag: make_still_working~2692
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=74d1ebeeda89c07bdd4d1807c20bd41bd023e74d;p=helm.git

Debugging disabled
---

diff --git a/matita/components/ng_paramodulation/nCicParamod.ml b/matita/components/ng_paramodulation/nCicParamod.ml
index 41d27cab9..ef9852fcc 100644
--- a/matita/components/ng_paramodulation/nCicParamod.ml
+++ b/matita/components/ng_paramodulation/nCicParamod.ml
@@ -16,9 +16,9 @@ NCicBlob.set_default_eqP()
 NCicProof.set_default_sig()
 ;;
 
-let debug _ = ();;
+let noprint _ = ();;
 let print s = prerr_endline (Lazy.force s);; 
-let debug = print;;
+let debug = noprint;; 
 
 module B(C : NCicBlob.NCicContext): Orderings.Blob 
   with type t = NCic.term and type input = NCic.term 
diff --git a/matita/components/ng_paramodulation/paramod.ml b/matita/components/ng_paramodulation/paramod.ml
index 7a63dd97a..86a964c14 100644
--- a/matita/components/ng_paramodulation/paramod.ml
+++ b/matita/components/ng_paramodulation/paramod.ml
@@ -13,7 +13,7 @@
 
 let print s = prerr_endline (Lazy.force s) ;; 
 let noprint s = ();;  
-let debug = print;;
+let debug = noprint;;
 
 let monster = 100;;
     
diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index af1d9f944..f4466fc1a 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -14,7 +14,7 @@ open Printf
 let print ?(depth=0) s = 
   prerr_endline (String.make depth '\t'^Lazy.force s) 
 let noprint ?(depth=0) _ = () 
-let debug_print = print
+let debug_print = noprint
 
 open Continuationals.Stack
 open NTacStatus