diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-06 14:42:23 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-06 14:42:23 +0000 |
| commit | 2bf066d9ffcacd7a78d4bc278f7a7909ce4f9a79 (patch) | |
| tree | 4b3d452205e53d6bafbfcfa9c6437ad932e4c5c5 /intf/vernacexpr.mli | |
| 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 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |