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 08e52ff72..66aef4d14 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -27,7 +27,7 @@ type cbv_value =
| VAL of int * constr
| STACK of int * cbv_value * cbv_stack
| CBN of constr * cbv_value subs
- | LAM of int * (name * constr) list * constr * cbv_value subs
+ | LAM of int * (Name.t * constr) list * constr * cbv_value subs
| FIXP of fixpoint * cbv_value subs * cbv_value array
| COFIXP of cofixpoint * cbv_value subs * cbv_value array
| CONSTR of constructor * cbv_value array