aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/reductionops.mli')
-rw-r--r--pretyping/reductionops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e67fad3fd..1e6527b29 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -296,5 +296,5 @@ val whd_betaiota_deltazeta_for_iota_state :
(** {6 Meta-related reduction functions } *)
val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
-val nf_meta : evar_map -> constr -> constr
+val nf_meta : evar_map -> EConstr.constr -> EConstr.constr
val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr