From 2bf066d9ffcacd7a78d4bc278f7a7909ce4f9a79 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 6 Jul 2012 14:42:23 +0000
Subject: 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
---
 parsing/g_vernac.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'parsing')

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)
 
-- 
cgit v1.2.3