diff options
| author | Gaëtan Gilbert | 2018-06-21 15:07:56 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-12 14:07:25 +0200 |
| commit | cb219011534a8de24a01ddb007799133cdd2cb0e (patch) | |
| tree | e754dd9853ef891c5daecfa6987881048f8952b1 /pretyping/reductionops.mli | |
| parent | 31fce698ec8c3186dc6af49961e8572e81cab50b (diff) | |
Cleanup reduction effects: they only work on constants.
We only ever call `reduction_effect_hook` on constants, so there's no
point allowing it to be declared with globrefs. There is also no point
using a constr map instead of constant map.
(Technically there was a call of the effect hook on projections, but
that can never match a globref so it was useless)
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 9256fa7ce6..bf8d6c710b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -41,10 +41,10 @@ val declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit (* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *) -val set_reduction_effect : GlobRef.t -> effect_name -> unit +val set_reduction_effect : Constant.t -> effect_name -> unit (* [effect_hook env sigma key term] apply effect associated to [key] on [term] *) -val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr -> +val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constant.t -> Constr.constr Lazy.t -> unit (** {6 Machinery about a stack of unfolded constant } |