diff options
| author | herbelin | 2011-12-18 15:03:21 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-18 15:03:21 +0000 |
| commit | 52210a54bd994ae3965c10391fa7bf29b74e6c56 (patch) | |
| tree | b5de9d95e8a58ec40e6fe18521ddbbf7bc019ba9 | |
| parent | be2b8dd639ae6609d306e49736557fe8432c12f2 (diff) | |
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
| -rw-r--r-- | parsing/g_proofs.ml4 | 12 |
1 files 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: |