aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cbv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cbv.mli')
-rw-r--r--pretyping/cbv.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 87a03abbd..b014af2c7 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -8,6 +8,7 @@
open Names
open Term
+open EConstr
open Environ
open CClosure
open Esubst
@@ -23,6 +24,9 @@ val cbv_norm : cbv_infos -> constr -> constr
(***********************************************************************
i This is for cbv debug *)
+
+open Term
+
type cbv_value =
| VAL of int * constr
| STACK of int * cbv_value * cbv_stack