diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index e6dd5c25c2..80dba10682 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -47,7 +47,7 @@ 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 *) +(* For compatibility: alias for whd\_stack *) val whd_castapp_stack : local_stack_reduction_function (*s Reduction Function Operators *) |