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/float64.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index 86b14c5cd2..07fb25734b 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -117,7 +117,7 @@ let frshiftexp f = m, Uint63.of_int (e + eshift) [@@ocaml.inline always] -let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) +let ldshiftexp f e = ldexp f (Uint63.to_int_min e (2 * eshift) - eshift) [@@ocaml.inline always] external next_up : float -> float = "coq_next_up_byte" "coq_next_up" -- cgit v1.2.3