From 6114cb246d344e93b0dfeae4d273dc4422633ecb Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 21 Oct 2011 06:49:56 +0000 Subject: [PATCH] Disabled debug. --- matita/components/grafite_parser/grafiteParser.ml | 3 +-- matita/components/ng_tactics/nnAuto.ml | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 16bc6c32e..720b4196a 100644 --- 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> (* ≝ *); 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 0b3cd9361..72099fbd3 100644 --- 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 -- 2.39.2