diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 93cb4c190c..140ebdc87d 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -143,10 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -(** {6 Reduction Function Operators } *) - -val strong : reduction_function -> reduction_function - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function |