aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/reductionops.mli')
-rw-r--r--pretyping/reductionops.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8aaeeb2c2..dcc11cfcf 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -156,11 +156,11 @@ val nf_beta : local_reduction_function
val nf_betaiota : local_reduction_function
val nf_betaiotazeta : local_reduction_function
val nf_all : reduction_function
-val nf_evar : evar_map -> Constr.constr -> Constr.constr
+val nf_evar : evar_map -> constr -> constr
(** Lazy strategy, weak head reduction *)
-val whd_evar : evar_map -> Constr.constr -> Constr.constr
+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