aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.mli
diff options
context:
space:
mode:
authorMaxime Dénès2014-04-06 12:41:26 -0400
committerMaxime Dénès2014-04-09 01:05:48 -0400
commitaa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (patch)
tree254b9d84ee42798a513bcd5aea032a6e552b2067 /kernel/nativevalues.mli
parentde61c7d77e49286622c4aebd56f2e87b0df93903 (diff)
Partial support for open terms in int31.
Diffstat (limited to 'kernel/nativevalues.mli')
-rw-r--r--kernel/nativevalues.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 150811b72c..4c918e1163 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -75,6 +75,7 @@ val mk_block : tag -> t array -> t
val mk_int : int -> t
+val mk_uint : Uint31.t -> t
val napply : t -> t array -> t
(* Functions over accumulators *)
@@ -110,3 +111,5 @@ val is_accu : t -> bool
val str_encode : 'a -> string
val str_decode : string -> 'a
+
+val mk_I31_accu : t