From 52210a54bd994ae3965c10391fa7bf29b74e6c56 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 18 Dec 2011 15:03:21 +0000
Subject: Removing PrintConstr debugging entry in g_proof.ml4 which was not
 working and was causing a warning when declaring the entry of same name in
 top_printers.ml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14815 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_proofs.ml4 | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 78299448ae..9abb8cd17d 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -88,7 +88,7 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
       | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis
       | IDENT "Guarded" -> VernacCheckGuard
-(* Hints for Auto and EAuto *)
+      (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
 	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
 	    VernacCreateHintDb (use_module_locality (), id, b)
@@ -97,18 +97,12 @@ GEXTEND Gram
       | IDENT "Hint"; local = obsolete_locality; h = hint;
 	  dbnames = opt_hintbases ->
 	  VernacHints (enforce_module_locality local,dbnames, h)
-
-(* Declare "Resolve" directly so as to be able to later extend with
-   "Resolve ->" and "Resolve <-" *)
+      (* Declare "Resolve" explicitly so as to be able to later extend with
+         "Resolve ->" and "Resolve <-" *)
       | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural;
 	  dbnames = opt_hintbases ->
 	  VernacHints (use_module_locality (),dbnames,
 	    HintsResolve (List.map (fun x -> (n, true, x)) lc))
-
-(*This entry is not commented, only for debug*)
-      | IDENT "PrintConstr"; c = constr ->
-	  VernacExtend ("PrintConstr",
-	    [Genarg.in_gen Genarg.rawwit_constr c])
       ] ];
 
   obsolete_locality:
-- 
cgit v1.2.3