From d39fab9a7c39d8da868c4481b96cf1086c21b1a4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 10 Oct 2019 20:11:02 +0200 Subject: Fix ldshiftexp * Fix the implementations and add tests * Change shift from int63 to Z (was always used as a Z) * Update FloatLemmas.v accordingly Co-authored-by: Erik Martin-Dorel --- kernel/uint63_63.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/uint63_63.ml') diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 1776f904d6..85b44528a7 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -27,8 +27,6 @@ let to_int2 i = (0,i) let of_int64 _i = assert false -let to_int_saturate i = i - let of_float = int_of_float external to_float : int -> (float [@unboxed]) @@ -104,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 *) -- cgit v1.2.3