diff options
| author | aspiwack | 2012-07-06 14:42:23 +0000 |
|---|---|---|
| committer | aspiwack | 2012-07-06 14:42:23 +0000 |
| commit | 2bf066d9ffcacd7a78d4bc278f7a7909ce4f9a79 (patch) | |
| tree | 4b3d452205e53d6bafbfcfa9c6437ad932e4c5c5 /parsing | |
| parent | 1e29aa8a28d53295279c6e51a52d96af6a41a2de (diff) | |
A prototype implementation of a Print Namespace command.
It is used as Print Namespace Coq.Init.
This prototypes only prints the name of constants (hence no inductive types).
The display order is a tad arbitrary too.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15537 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 509d266be8..40cf0d06d9 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -768,6 +768,8 @@ GEXTEND Gram VernacPrint (PrintModuleType qid) | IDENT "Print"; IDENT "Module"; qid = global -> VernacPrint (PrintModule qid) + | IDENT "Print"; IDENT "Namespace" ; ns = dirpath -> + VernacPrint (PrintNamespace ns) | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid) |