From dda50a88aab0fa0cfb74c8973b5a4353fe5c8447 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Fri, 3 Aug 2018 17:38:48 +0200
Subject: Put axioms on ldshiftexp and frshiftexp

Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas.

The shift value has been increased to 2 * emax + prec because in ldexp
we want to be able to transform the smallest denormalized to the biggest
float value in one call.
---
 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 0b22e07e82..a625c0f551 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -51,7 +51,7 @@ let normfr_mantissa f =
   if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec)
   else Uint63.zero
 
-let eshift = 1022 + 52 (* minimum negative exponent + binary precision *)
+let eshift = 2101 (* 2*emax + prec *)
 
 (* When calling frexp on a nan or an infinity, the returned value inside
    the exponent is undefined.
-- 
cgit v1.2.3