diff options
| author | Maxime Dénès | 2017-11-28 11:10:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-28 11:10:56 +0100 |
| commit | 24adb2ee00b860f4550d05bd38dde4a284bcd7bc (patch) | |
| tree | 2c32fc1aa8724ab4685c6a9a0e568eb49132d9f5 /parsing | |
| parent | ddfca160f14eba979bcaa238da4c91e4e445f37b (diff) | |
| parent | d1d18519cfcf0787203b73fb050f76355ff26adf (diff) | |
Merge PR #1033: Universe binder improvements
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 a01ea26af2..0e585cff77 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 |