diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-04-29 09:32:44 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-04-29 09:32:44 +0200 |
commit | 4920f93e4f933c8616a3376da5264d63bd58afdc (patch) | |
tree | f05cdd8084fcbc2098bbad14dc5b3fe38bf34ba4 /flocq/Prop/Plus_error.v | |
parent | fb1f4545dfe861ff4d02816e295021a7e3061687 (diff) | |
parent | e8c312eecf96ae1703f7ba0b65f107233d340238 (diff) | |
download | compcert-4920f93e4f933c8616a3376da5264d63bd58afdc.tar.gz compcert-4920f93e4f933c8616a3376da5264d63bd58afdc.zip |
Merge pull request #368 from silene/flocq-3.4
Upgrade to Flocq 4.1.
Diffstat (limited to 'flocq/Prop/Plus_error.v')
-rw-r--r-- | flocq/Prop/Plus_error.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/flocq/Prop/Plus_error.v b/flocq/Prop/Plus_error.v index 514d3aab..bf0b28cd 100644 --- a/flocq/Prop/Plus_error.v +++ b/flocq/Prop/Plus_error.v @@ -19,11 +19,9 @@ COPYING file for more details. (** * Error of the rounded-to-nearest addition is representable. *) -Require Import Psatz. -Require Import Raux Defs Float_prop Generic_fmt. -Require Import FIX FLX FLT Ulp Operations. -Require Import Relative. +From Coq Require Import ZArith Reals Psatz. +Require Import Core Operations Relative. Section Fprop_plus_error. @@ -519,7 +517,7 @@ rewrite <- mag_minus1; try assumption. unfold FLT_exp; apply bpow_le. apply Z.le_trans with (2:=Z.le_max_l _ _). destruct (mag beta x) as (n,Hn); simpl. -assert (e + prec < n)%Z; try lia. +cut (e + prec < n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. @@ -567,7 +565,7 @@ unfold cexp. rewrite <- mag_minus1 by easy. unfold FLX_exp; apply bpow_le. destruct (mag beta x) as (n,Hn); simpl. -assert (e + prec < n)%Z; try lia. +cut (e + prec < n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. |