From dce9ff8da2710aa81fbcf6d1498de35ea9ad06f4 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 13 Feb 2017 10:28:35 +0100
Subject: Update Flocq to version 2.5.2

This version of Flocq is compatible with Coq 8.6
---
 flocq/Core/Fcore_ulp.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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

diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v
index 1c27de31..28d2bc35 100644
--- a/flocq/Core/Fcore_ulp.v
+++ b/flocq/Core/Fcore_ulp.v
@@ -35,6 +35,7 @@ Variable fexp : Z -> Z.
 (** Definition and basic properties about the minimal exponent, when it exists *)
 
 Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z.
+Proof.
 intros.
 destruct (Z_le_dec x y).
 now left.
@@ -158,8 +159,7 @@ rewrite ulp_neq_0.
 unfold F2R; simpl.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
-replace 1%R with (Z2R (Zsucc 0)) by reflexivity.
-apply Z2R_le.
+apply (Z2R_le (Zsucc 0)).
 apply Zlt_le_succ.
 apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
 now rewrite <- Fx.
@@ -206,6 +206,7 @@ Qed.
 
 Theorem ulp_bpow :
   forall e, ulp (bpow e) = bpow (fexp (e + 1)).
+Proof.
 intros e.
 rewrite ulp_neq_0.
 apply f_equal.
-- 
cgit