diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 600cdd8230..794c493544 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -59,16 +59,19 @@ val nf_betadeltaiota : 'a reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betadeltaiota : 'a contextual_reduction_function +val whd_betadeltaiota_nolet : 'a contextual_reduction_function val whd_betaetalet : local_reduction_function val whd_beta_stack : local_stack_reduction_function val whd_betaiota_stack : local_stack_reduction_function val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function +val whd_betadeltaiota_nolet_stack : 'a contextual_stack_reduction_function val whd_betaetalet_stack : local_stack_reduction_function val whd_beta_state : local_state_reduction_function val whd_betaiota_state : local_state_reduction_function val whd_betadeltaiota_state : 'a contextual_state_reduction_function +val whd_betadeltaiota_nolet_state : 'a contextual_state_reduction_function val whd_betaetalet_state : local_state_reduction_function (*s Head normal forms *) |