Disabled debug.

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 16bc6c32ebe60a3efd8537a23ed9a42b4d483de2..720b4196a2c6d4908d0811c6620d6bcb15ac9aef 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -538,8 +538,7 @@ EXTEND
   grafite_ncommand: [ [
       IDENT "qed" ;  b = OPT SYMBOL "-" -> 
       let b = match b with None -> true | Some _ -> false in
-      if not b then prerr_endline "Should not index";
-      G.NQed (loc,b)
+      if not b then G.NQed (loc,b)
     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 0b3cd9361fadac7af05dbcfbc3d53f73f4bf2f4f..72099fbd3ead131956f9ad0e1c142a389ef3c3c6 100644 (file)
--- 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 (2*depth) ' '^Lazy.force s) 
 let noprint ?(depth=0) _ = () 
-let debug_print = print
+let debug_print = noprint
 
 open Continuationals.Stack
 open NTacStatus