aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/vnorm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/vnorm.mli')
-rw-r--r--pretyping/vnorm.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index bc6eec851..650f3f291 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -6,8 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
+open EConstr
open Environ
(** {6 Reduction functions } *)
-val cbv_vm : env -> Evd.evar_map -> constr -> types -> constr
+val cbv_vm : env -> Evd.evar_map -> constr -> types -> Constr.t