diff options
| author | Pierre-Marie Pédrot | 2020-04-01 17:39:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-10 15:04:06 +0200 |
| commit | cf60564b9e6cdfa35fe8c256f6785e23a2afde61 (patch) | |
| tree | c647d30d9d8ed572ff43717c09f0d0c55356cb9a /pretyping/reductionops.mli | |
| parent | 2a79abc613bdf19b53685a40c993f964455904fe (diff) | |
Further cleanup: remove the local_reduction_function type.
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 555c4be971..be91f688e7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -128,7 +128,6 @@ end type state = constr * constr Stack.t type reduction_function = env -> evar_map -> constr -> constr -type local_reduction_function = evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr @@ -150,8 +149,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) -> (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -val local_strong : local_reduction_function -> local_reduction_function -val strong_prodspine : local_reduction_function -> local_reduction_function (*i val stack_reduction_of_reduction : 'a reduction_function -> 'a state_reduction_function |