aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.mli
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-27 10:06:39 +0000
committerGitHub2021-02-27 10:06:39 +0000
commit3915bc904fc16060c25baaf7d5626e3587ad2891 (patch)
tree81c21fc95c1790250396119583a57ef4b6f1f3a1 /kernel/nativevalues.mli
parent1e54fe53ac47f08d7b8f13df16487b5a2639404f (diff)
parent4302a75d82b9ac983cd89dd01c742c36777d921b (diff)
Merge PR #13559: Signed primitive integers
Reviewed-by: SkySkimmer Reviewed-by: silene Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: proux01
Diffstat (limited to 'kernel/nativevalues.mli')
-rw-r--r--kernel/nativevalues.mli23
1 files changed, 23 insertions, 0 deletions
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index b9b75a9d7c..98cf4219a0 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -158,9 +158,12 @@ val sub : t -> t -> t -> t
val mul : t -> t -> t -> t
val div : t -> t -> t -> t
val rem : t -> t -> t -> t
+val divs : t -> t -> t -> t
+val rems : t -> t -> t -> t
val l_sr : t -> t -> t -> t
val l_sl : t -> t -> t -> t
+val a_sr : t -> t -> t -> t
val l_and : t -> t -> t -> t
val l_xor : t -> t -> t -> t
val l_or : t -> t -> t -> t
@@ -179,7 +182,10 @@ val addMulDiv : t -> t -> t -> t -> t
val eq : t -> t -> t -> t
val lt : t -> t -> t -> t
val le : t -> t -> t -> t
+val lts : t -> t -> t -> t
+val les : t -> t -> t -> t
val compare : t -> t -> t -> t
+val compares : t -> t -> t -> t
val print : t -> t
@@ -205,12 +211,21 @@ val no_check_div : t -> t -> t
val no_check_rem : t -> t -> t
[@@ocaml.inline always]
+val no_check_divs : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_rems : t -> t -> t
+[@@ocaml.inline always]
+
val no_check_l_sr : t -> t -> t
[@@ocaml.inline always]
val no_check_l_sl : t -> t -> t
[@@ocaml.inline always]
+val no_check_a_sr : t -> t -> t
+[@@ocaml.inline always]
+
val no_check_l_and : t -> t -> t
[@@ocaml.inline always]
@@ -253,8 +268,16 @@ val no_check_lt : t -> t -> t
val no_check_le : t -> t -> t
[@@ocaml.inline always]
+val no_check_lts : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_les : t -> t -> t
+[@@ocaml.inline always]
+
val no_check_compare : t -> t -> t
+val no_check_compares : t -> t -> t
+
(** Support for machine floating point values *)
val is_float : t -> bool