From 9c3fc6c4e2579facfd3ca4b80e87b1c1f9672e2e Mon Sep 17 00:00:00 2001
From: Sylvie Boldo <sylvie.boldo@inria.fr>
Date: Tue, 21 Sep 2010 08:18:20 +0000
Subject: [PATCH] Change of stating of canonic_exp_ge

---
 src/Core/Fcore_generic_fmt.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v
index d47513a..7f45f52 100644
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -303,7 +303,7 @@ Qed.
 
 Theorem canonic_exp_ge:
   forall prec,
-  (forall e, (e-prec <= fexp e)%Z) ->
+  (forall e, (e-fexp e <= prec)%Z) ->
   (* OK with FLX, FLT and FTZ *)
   forall x, generic_format x ->
   (Rabs x < bpow (prec + canonic_exponent x))%R.
-- 
GitLab