diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ac81786b..333934be 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -143,7 +143,7 @@ let test_plurial_form_types = function (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - typeclass_constraint record_field decl_notation rec_definition; + record_field decl_notation rec_definition; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -656,6 +656,7 @@ GEXTEND Gram | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits] | IDENT "clear"; IDENT "scopes" -> [`ClearScopes] | IDENT "rename" -> [`Rename] + | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes] | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" -> [`ClearImplicits; `ClearScopes] | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" -> @@ -927,7 +928,6 @@ GEXTEND Gram (* Resetting *) | IDENT "Reset"; id = identref -> VernacResetName id - | IDENT "Delete"; id = identref -> VernacRemoveName id | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n |