diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d5ff2538c4..371dae6c81 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -629,10 +629,10 @@ GEXTEND Gram error "All arguments lists must have the same length"; let err_incompat x y = error ("Options \""^x^"\" and \""^y^"\" are incompatible") in - if nargs > 0 && List.mem `SimplNeverUnfold mods then + if nargs > 0 && List.mem `ReductionNeverUnfold mods then err_incompat "simpl never" "/"; - if List.mem `SimplNeverUnfold mods && - List.mem `SimplDontExposeCase mods then + if List.mem `ReductionNeverUnfold mods && + List.mem `ReductionDontExposeCase mods then err_incompat "simpl never" "simpl nomatch"; VernacArguments (qid, impl, nargs, mods) @@ -665,8 +665,8 @@ GEXTEND Gram VernacGeneralizable gen ] ] ; arguments_modifier: - [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase] - | IDENT "simpl"; IDENT "never" -> [`SimplNeverUnfold] + [ [ IDENT "simpl"; IDENT "nomatch" -> [`ReductionDontExposeCase] + | IDENT "simpl"; IDENT "never" -> [`ReductionNeverUnfold] | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits] | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits] | IDENT "clear"; IDENT "scopes" -> [`ClearScopes] |