diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 54ce527ea2..8a94a010a0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1048,6 +1048,7 @@ GRAMMAR EXTEND Gram | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> { PrintCoercionPaths (s,t) } | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions } + | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags } | IDENT "Tables" -> { PrintTables } | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) } | IDENT "Hint" -> { PrintHintGoal } |