From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 23 Nov 2010 14:06:30 +0000 (+0000)
Subject: Debugging code commented out.
X-Git-Tag: make_still_working~2685
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95b2fec522138b2a17e6f8ddc71683eb9dbf3413;p=helm.git

Debugging code commented out.
---

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 344e7535c..7a9c20f0f 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1740,7 +1740,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
                 oldstatus#set_status s 
   in
   let s = up_to depth depth in
-    print (print_stat statistics);
+    debug_print (print_stat statistics);
     debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
     debug_print(lazy