diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1d0a5ab0a3..960e74827a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -989,8 +989,9 @@ GRAMMAR EXTEND Gram | IDENT "Scope"; s = IDENT -> { PrintScope s } | IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s } | IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid } - | IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (false, fopt) } - | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (true, fopt) } + | b = [ IDENT "Sorted" -> { true } | -> { false } ]; IDENT "Universes"; + g = OPT printunivs_subgraph; fopt = OPT ne_string -> + { PrintUniverses (b, g, fopt) } | IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) } | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) } | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) } @@ -1000,6 +1001,9 @@ GRAMMAR EXTEND Gram | IDENT "Registered" -> { PrintRegistered } ] ] ; + printunivs_subgraph: + [ [ IDENT "Subgraph"; "("; l = LIST0 reference; ")" -> { l } ] ] + ; class_rawexpr: [ [ IDENT "Funclass" -> { FunClass } | IDENT "Sortclass" -> { SortClass } |