diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 362fbcfc8c..ebf456301f 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -44,8 +44,12 @@ type 'a contextual_state_reduction_function = type 'a state_reduction_function = 'a contextual_state_reduction_function type local_state_reduction_function = state -> state +(* Removes cast and put into applicative form *) val whd_stack : local_stack_reduction_function +(* For compatibility: alias for whd_stack *) +val whd_castapp_stack : local_stack_reduction_function + (*s Reduction Function Operators *) val strong : 'a reduction_function -> 'a reduction_function |