aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cbv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cbv.mli')
-rw-r--r--pretyping/cbv.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 87a03abbd..3d1745767 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -19,7 +19,7 @@ open Esubst
type cbv_infos
val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos
-val cbv_norm : cbv_infos -> constr -> constr
+val cbv_norm : cbv_infos -> EConstr.constr -> constr
(***********************************************************************
i This is for cbv debug *)