diff options
| author | Pierre Boutillier | 2014-02-04 15:19:25 +0100 |
|---|---|---|
| committer | Pierre Boutillier | 2014-02-24 14:07:07 +0100 |
| commit | a6dedd0d1184ae67c6ff48323f2df17dc1d42ef2 (patch) | |
| tree | d4b5e4fbc7704caa4eddab5033f8fdabc632ae24 /parsing | |
| parent | cbee386324fa6384c4f251d83ed70e84e1290142 (diff) | |
Simpl_behaviour becomes Reductionops.ReductionBehaviour
syntax mentionning simpl remains
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] |