diff options
Diffstat (limited to 'kernel/uint63_63.ml')
| -rw-r--r-- | kernel/uint63_63.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 5c4028e1c8..85b44528a7 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -27,6 +27,12 @@ let to_int2 i = (0,i) let of_int64 _i = assert false +let of_float = int_of_float + +external to_float : int -> (float [@unboxed]) + = "coq_uint63_to_float_byte" "coq_uint63_to_float" +[@@noalloc] + let hash i = i [@@ocaml.inline always] @@ -96,6 +102,10 @@ let le (x : int) (y : int) = (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000) [@@ocaml.inline always] +let to_int_min n m = + if lt n m then n else m +[@@ocaml.inline always] + (* division of two numbers by one *) (* precondition: xh < y *) (* outputs: q, r s.t. x = q * y + r, r < y *) |