diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-20 19:45:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | 280c922fc55b57c430cad721c83650a796a375fd (patch) | |
| tree | 5f0c9c20a75532ba134bbde6f428facefceb5125 /parsing | |
| parent | c93d5094bff73498ec8fc02837e16cc5ce9103b6 (diff) | |
Allow local universe renaming in Print.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a01ea26af..0e585cff7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -875,7 +875,7 @@ GEXTEND Gram (* Printing (careful factorization of entries) *) | IDENT "Print"; p = printable -> VernacPrint p - | IDENT "Print"; qid = smart_global -> VernacPrint (PrintName qid) + | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> VernacPrint (PrintName (qid,l)) | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> VernacPrint (PrintModuleType qid) | IDENT "Print"; IDENT "Module"; qid = global -> @@ -940,8 +940,8 @@ GEXTEND Gram | IDENT "Check"; c = lconstr; "." -> fun g -> VernacCheckMayEval (None, g, c) (* Searching the environment *) - | IDENT "About"; qid = smart_global; "." -> - fun g -> VernacPrint (PrintAbout (qid,g)) + | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." -> + fun g -> VernacPrint (PrintAbout (qid,l,g)) | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchHead c,g, l) | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> @@ -960,7 +960,7 @@ GEXTEND Gram ] ] ; printable: - [ [ IDENT "Term"; qid = smart_global -> PrintName qid + [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> PrintName (qid,l) | IDENT "All" -> PrintFullContext | IDENT "Section"; s = global -> PrintSectionContext s | IDENT "Grammar"; ent = IDENT -> @@ -1060,6 +1060,9 @@ GEXTEND Gram | -> ([],SearchOutside []) ] ] ; + univ_name_list: + [ [ "@{" ; l = LIST0 name; "}" -> l ] ] + ; END; GEXTEND Gram |