From 2bf066d9ffcacd7a78d4bc278f7a7909ce4f9a79 Mon Sep 17 00:00:00 2001
From: aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf/vernacexpr.mli')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 37f25e0ac..d4d30dce8 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -42,6 +42,7 @@ type printable =
   | PrintModules
   | PrintModule of reference
   | PrintModuleType of reference
+  | PrintNamespace of dir_path
   | PrintMLLoadPath
   | PrintMLModules
   | PrintName of reference or_by_notation
-- 
cgit v1.2.3