diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a0ee06683f..3bc27965ab 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -553,9 +553,11 @@ GEXTEND Gram | IDENT "Implicit"; ["Type" | IDENT "Types"]; idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) - | IDENT "Generalizable"; ["Variable" | IDENT "Variables"]; - gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | - idl = LIST1 identref -> Some idl ] -> + | IDENT "Generalizable"; + gen = [IDENT "All"; IDENT "Variables" -> Some [] + | IDENT "No"; IDENT "Variables" -> None + | [IDENT "Variable" | IDENT "Variables"]; + idl = LIST1 identref -> Some idl ] -> VernacGeneralizable (use_non_locality (), gen) ] ] ; implicit_name: |