diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-19 10:35:50 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-19 10:35:50 +0000 |
| commit | 99843b6c0c9ac9e7f9e75a2a3361211e67d31d89 (patch) | |
| tree | dc59d885d61568677a7a067fbd13fc0483c9adf3 /parsing/g_basevernac.ml4 | |
| parent | a3a5350786ace6fac2c12890df6330782201cc77 (diff) | |
Pretty-printing preliminaire des modules, commandes
Print Module qid.
Print Module Type qid.
et affichage pendant
Print All.
Tout ca est preliminare, seuls les noms des composants sont affiches et
non pas les corps...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_basevernac.ml4')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index b535f1e24..ede831944 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -79,6 +79,10 @@ GEXTEND Gram | IDENT "Print"; p = printable -> VernacPrint p | IDENT "Print"; qid = qualid -> VernacPrint (PrintName qid) | IDENT "Print" -> VernacPrint PrintLocalContext + | IDENT "Print"; IDENT "Module"; "Type"; qid = qualid -> + VernacPrint (PrintModuleType qid) + | IDENT "Print"; IDENT "Module"; qid = qualid -> + VernacPrint (PrintModule qid) | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) (* Searching the environment *) |