diff options
| author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-08 08:35:29 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-08 08:35:29 +0100 |
| commit | 177c8fbc523a171e8c8470fa675f9a69ef7f99de (patch) | |
| tree | f54d8315891bec2f741545991f420dd4407bccc0 /flocq/Core/Fcore_rnd_ne.v | |
| parent | 44b63eb13151ca5c3e83ee6a9e7eb6c0049c3758 (diff) | |
| download | compcert-kvx-177c8fbc523a171e8c8470fa675f9a69ef7f99de.tar.gz compcert-kvx-177c8fbc523a171e8c8470fa675f9a69ef7f99de.zip | |
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_rnd_ne.v')
| -rw-r--r-- | flocq/Core/Fcore_rnd_ne.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v index 1f265406..2d67e709 100644 --- a/flocq/Core/Fcore_rnd_ne.v +++ b/flocq/Core/Fcore_rnd_ne.v @@ -370,7 +370,7 @@ destruct (Rle_or_lt (round beta fexp Zfloor x) 0) as [Hr|Hr]. rewrite (Rle_antisym _ _ Hr). unfold scaled_mantissa. rewrite Rmult_0_l. -change R0 with (Z2R 0). +change 0%R with (Z2R 0). now rewrite (Ztrunc_Z2R 0). rewrite <- (round_0 beta fexp Zfloor). apply round_le... |