diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-03-08 14:07:33 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-03-08 14:07:33 +0100 |
| commit | a968152051941a0fc50a86c3fc15e90e22ed7c47 (patch) | |
| tree | 70f2590a8ea026c2f8596220e60b829d21b6398c /flocq/Core/Fcore_FTZ.v | |
| parent | de24549f572deb6519be2216ef364b7c80bfdece (diff) | |
| parent | 177c8fbc523a171e8c8470fa675f9a69ef7f99de (diff) | |
| download | compcert-a968152051941a0fc50a86c3fc15e90e22ed7c47.tar.gz compcert-a968152051941a0fc50a86c3fc15e90e22ed7c47.zip | |
Merge pull request #175 from silene/IZR
Adapt proofs to future handling of literal constants in Coq
This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
Diffstat (limited to 'flocq/Core/Fcore_FTZ.v')
| -rw-r--r-- | flocq/Core/Fcore_FTZ.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/flocq/Core/Fcore_FTZ.v b/flocq/Core/Fcore_FTZ.v index 2ebc7851..a2fab00b 100644 --- a/flocq/Core/Fcore_FTZ.v +++ b/flocq/Core/Fcore_FTZ.v @@ -217,7 +217,7 @@ Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. Definition Zrnd_FTZ x := - if Rle_bool R1 (Rabs x) then rnd x else Z0. + if Rle_bool 1 (Rabs x) then rnd x else Z0. Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ. Proof with auto with typeclass_instances. @@ -270,7 +270,7 @@ Proof. intros x Hx. unfold round, scaled_mantissa, canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. -assert (Hx0: x <> R0). +assert (Hx0: x <> 0%R). intros Hx0. apply Rle_not_lt with (1 := Hx). rewrite Hx0, Rabs_R0. @@ -286,7 +286,7 @@ rewrite Rle_bool_true. apply refl_equal. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))). -change R1 with (bpow 0). +change 1%R with (bpow 0). rewrite <- (Zplus_opp_r (FLX_exp prec ex)). rewrite bpow_plus. apply Rmult_le_compat_r. @@ -320,7 +320,7 @@ rewrite Rle_bool_false. apply F2R_0. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))). -change R1 with (bpow 0). +change 1%R with (bpow 0). rewrite <- (Zplus_opp_r (FTZ_exp ex)). rewrite bpow_plus. apply Rmult_lt_compat_r. |