diff options
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) |