aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativevalues.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativevalues.mli')
-rw-r--r--kernel/nativevalues.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 4c918e116..821b23168 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -113,3 +113,4 @@ val str_encode : 'a -> string
val str_decode : string -> 'a
val mk_I31_accu : t
+val decomp_uint : t -> t -> t