From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Mar 2010 11:28:22 +0000 (+0000)
Subject: Debugging disabled.
X-Git-Tag: make_still_working~2991
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1eaf58f3b0f2f7a871f627bcea36c8d04d8309e2;p=helm.git

Debugging disabled.
---

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index f314d3eb3..2a221a213 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -172,7 +172,7 @@ let solve f status eq_cache goal =
   let gty = NCicUntrusted.apply_subst subst ctx gty in
   let build_status (pt, _, metasenv, subst) =
     try
-      print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+      debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
       let stamp = Unix.gettimeofday () in 
       let metasenv, subst, pt, pty =
 	(* NCicRefiner.typeof status