diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -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 b98a7d309..664039206 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -115,6 +115,7 @@ val nf_betaiota_preserving_vm_cast : reduction_function (** Lazy strategy, weak head reduction *) val whd_evar : evar_map -> constr -> constr +val whd_nored : local_reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function |