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 /toplevel | |
| parent | cbee386324fa6384c4f251d83ed70e84e1290142 (diff) | |
Simpl_behaviour becomes Reductionops.ReductionBehaviour
syntax mentionning simpl remains
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 51fbbc47bb..cd2338dfe5 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -993,13 +993,13 @@ let vernac_declare_arguments locality r l nargs flags = if nargs >= 0 && nargs < List.fold_left max 0 rargs then error "The \"/\" option must be placed after the last \"!\"."; let rec narrow = function - | #Tacred.simpl_flag as x :: tl -> x :: narrow tl + | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl | [] -> [] | _ :: tl -> narrow tl in let flags = narrow flags in if not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) then match sr with | ConstRef _ as c -> - Tacred.set_simpl_behaviour + Reductionops.ReductionBehaviour.set (make_section_locality locality) c (rargs, nargs, flags) | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.") |