diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 436648c163..69ab0fafe9 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1026,7 +1026,8 @@ GRAMMAR EXTEND Gram | IDENT "Coercions" -> { PrintCoercions } | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> { PrintCoercionPaths (s,t) } - | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions } + | IDENT "Canonical"; IDENT "Projections"; qids = LIST0 smart_global + -> { PrintCanonicalConversions qids } | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags } | IDENT "Tables" -> { PrintTables } | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) } |