aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmvalues.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vmvalues.mli')
-rw-r--r--kernel/vmvalues.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index ae1d416ed5..6d984d5f49 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -44,6 +44,7 @@ type structured_constant =
| Const_b0 of tag
| Const_univ_level of Univ.Level.t
| Const_val of structured_values
+ | Const_uint of Uint63.t
val pp_struct_const : structured_constant -> Pp.t
@@ -125,6 +126,7 @@ type whd =
| Vcofix of vcofix * to_update * arguments option
| Vconstr_const of int
| Vconstr_block of vblock
+ | Vint64 of int64
| Vatom_stk of atom * stack
| Vuniv_level of Univ.Level.t
@@ -145,6 +147,7 @@ val val_of_proj : Projection.Repr.t -> values -> values
val val_of_atom : atom -> values
val val_of_int : int -> structured_values
val val_of_block : tag -> structured_values array -> structured_values
+val val_of_uint : Uint63.t -> structured_values
external val_of_annot_switch : annot_switch -> values = "%identity"
external val_of_proj_name : Projection.Repr.t -> values = "%identity"