From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Oct 2011 12:34:52 +0000 (+0000)
Subject: Debugging code commented out.
X-Git-Tag: make_still_working~2227
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cef076c6fbd4ceec7c460414cf4421611457188d;p=helm.git

Debugging code commented out.
---

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 9ea4dc03d..23ad46494 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1722,7 +1722,7 @@ auto_main flags signature cache depth status: unit =
               let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
               mk_cic_term ctx dty 
             in 
-            prerr_endline ("FAILURE : " ^ ppterm status gty);
+            (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
             add_to_th newfail failures closegty
           else failures in
         debug_print ~depth (lazy "no more candidates");