diff options
| author | Pierre-Marie Pédrot | 2018-07-25 15:56:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-25 15:56:49 +0200 |
| commit | 523de4f878293cf1d582bd70300b34d497e705b3 (patch) | |
| tree | 5037ac2e2fd60003d582d800466657df624b848f /pretyping/reductionops.mli | |
| parent | 9b6ce4f1848c546d0d361aa1089fa2907ca4c9ad (diff) | |
| parent | cb219011534a8de24a01ddb007799133cdd2cb0e (diff) | |
Merge PR #7889: Cleanup reduction effects: they only work on constants.
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 b44c642d43..07eeec9276 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 } |