diff options
| -rw-r--r-- | pretyping/reductionops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index a8d991cae..5cf0bfd91 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -79,6 +79,7 @@ val whd_betadeltaiota_stack : contextual_stack_reduction_function val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function val whd_betaetalet_stack : local_stack_reduction_function +val whd_state : local_state_reduction_function val whd_beta_state : local_state_reduction_function val whd_betaiota_state : local_state_reduction_function val whd_betaiotazeta_state : local_state_reduction_function |