From 0af966a42eb60e9af43f9a450d924758a83946c6 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 22 Sep 2015 15:41:50 +0200
Subject: Upgrade to Flocq 2.5.0.

Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.
---
 flocq/Core/Fcore_FIX.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'flocq/Core/Fcore_FIX.v')

diff --git a/flocq/Core/Fcore_FIX.v b/flocq/Core/Fcore_FIX.v
index a3b8d4d0..e224a64a 100644
--- a/flocq/Core/Fcore_FIX.v
+++ b/flocq/Core/Fcore_FIX.v
@@ -22,6 +22,7 @@ Require Import Fcore_Raux.
 Require Import Fcore_defs.
 Require Import Fcore_rnd.
 Require Import Fcore_generic_fmt.
+Require Import Fcore_ulp.
 Require Import Fcore_rnd_ne.
 
 Section RND_FIX.
@@ -84,4 +85,16 @@ intros ex ey H.
 apply Zle_refl.
 Qed.
 
+Theorem ulp_FIX: forall x, ulp beta FIX_exp x = bpow emin.
+Proof.
+intros x; unfold ulp.
+case Req_bool_spec; intros Zx.
+case (negligible_exp_spec FIX_exp).
+intros T; specialize (T (emin-1)%Z); contradict T.
+unfold FIX_exp; omega.
+intros n _; reflexivity.
+reflexivity.
+Qed.
+
+
 End RND_FIX.
-- 
cgit