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/byterun/coq_values.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 14f3f152bf..fa51b2d31f 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -45,6 +45,6 @@
 #define coq_tag_Some 1
 #define coq_None Val_int(0)
 
-#define FLOAT_EXP_SHIFT (1022 + 52)
+#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */
 
 #endif /* _COQ_VALUES_ */
-- 
cgit v1.2.3