From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 27 Mar 2011 13:07:45 +0000 (+0000)
Subject: Debugging code commented out.
X-Git-Tag: make_still_working~2544
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a4853a9af9f11750976a6bdd5eecaab51ed928f6;p=helm.git

Debugging code commented out.
---

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 020b819c9..7d57a9785 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1710,7 +1710,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
   app_counter:= 0;
   let rec up_to x y =
     if x > y then
-      (print(lazy
+      (debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
        debug_print(lazy
         ("Applicative nodes:"^string_of_int !app_counter));