diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2020-09-08 18:29:00 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-04-25 16:38:45 +0200 |
commit | 9aacc59135071a979623ab177819cdbe9ce27056 (patch) | |
tree | 1d2069eba895833fdb3a7647c3cc37cea32a0de6 /flocq/Core/Ulp.v | |
parent | fb1f4545dfe861ff4d02816e295021a7e3061687 (diff) | |
download | compcert-9aacc59135071a979623ab177819cdbe9ce27056.tar.gz compcert-9aacc59135071a979623ab177819cdbe9ce27056.zip |
Upgrade to Flocq 4.0.
Diffstat (limited to 'flocq/Core/Ulp.v')
-rw-r--r-- | flocq/Core/Ulp.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/flocq/Core/Ulp.v b/flocq/Core/Ulp.v index c42b3e65..2459e35b 100644 --- a/flocq/Core/Ulp.v +++ b/flocq/Core/Ulp.v @@ -18,8 +18,10 @@ COPYING file for more details. *) (** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *) -Require Import Reals Psatz. -Require Import Raux Defs Round_pred Generic_fmt Float_prop. + +From Coq Require Import ZArith Reals Psatz. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop. Section Fcore_ulp. @@ -1100,7 +1102,7 @@ exfalso ; lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. -assert(mag beta eps-1 < fexp n)%Z;[idtac|lia]. +cut (mag beta eps-1 < fexp n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (2:=proj2 H). destruct (mag beta eps) as (e,He). @@ -1165,7 +1167,7 @@ lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. -assert(mag beta eps-1 < fexp n)%Z;[idtac|lia]. +cut (mag beta eps-1 < fexp n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (2:=H). destruct (mag beta eps) as (e,He). @@ -1919,7 +1921,7 @@ rewrite ulp_neq_0; trivial. apply f_equal. unfold cexp. apply valid_exp; trivial. -assert (mag beta x -1 < fexp n)%Z;[idtac|lia]. +cut (mag beta x -1 < fexp n)%Z. lia. apply lt_bpow with beta. destruct (mag beta x) as (e,He). simpl. |