aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativelambda.mli')
-rw-r--r--kernel/nativelambda.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 98314348a..751f11978 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -32,6 +32,7 @@ type lambda =
(* A fully applied constructor *)
| Lconstruct of string * constructor (* prefix, constructor name *)
(* A partially applied constructor *)
+ | Luint of Uint31.t
| Lval of Nativevalues.t
| Lsort of sorts
| Lind of string * inductive (* prefix, inductive name *)