diff options
| author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-22 15:41:50 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-22 15:41:50 +0200 |
| commit | 0af966a42eb60e9af43f9a450d924758a83946c6 (patch) | |
| tree | 2bef73e80a8a80da1c47deee66dc825feac45bdd /flocq/Core/Fcore_rnd_ne.v | |
| parent | c212ab7a8adea516db72f17d818393629dbde1b3 (diff) | |
| download | compcert-0af966a42eb60e9af43f9a450d924758a83946c6.tar.gz compcert-0af966a42eb60e9af43f9a450d924758a83946c6.zip | |
Upgrade to Flocq 2.5.0.
Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.
Diffstat (limited to 'flocq/Core/Fcore_rnd_ne.v')
| -rw-r--r-- | flocq/Core/Fcore_rnd_ne.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v index 6829c0c8..1f265406 100644 --- a/flocq/Core/Fcore_rnd_ne.v +++ b/flocq/Core/Fcore_rnd_ne.v @@ -164,7 +164,7 @@ now apply Rlt_le. assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now apply valid_exp. assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R). rewrite Hxu, Hxd. -now apply ulp_DN_UP. +now apply round_UP_DN_ulp. destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2]. (* - xu > bpow ex *) elim (Rlt_not_le _ _ Hu2). @@ -191,7 +191,8 @@ rewrite Rmult_plus_distr_r. rewrite Z2R_Zpower, <- bpow_plus. ring_simplify (ex - fexp ex + fexp ex)%Z. rewrite Hu2, Hud. -unfold ulp, canonic_exp. +rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. +unfold canonic_exp. rewrite ln_beta_unique with beta x ex. unfold F2R. simpl. ring. @@ -223,7 +224,8 @@ specialize (H ex). omega. (* - xu < bpow ex *) revert Hud. -unfold ulp, F2R. +rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. +unfold F2R. rewrite Hd, Hu. unfold canonic_exp. rewrite ln_beta_unique with beta (F2R xu) ex. |