diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-25 11:47:59 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-25 11:47:59 +0200 |
commit | 2dd133f9178ae285d3939f29479b4acd9dad394d (patch) | |
tree | a89023c15848438f84b47663633f34960b9bcfbc /flocq/IEEE754/Bits.v | |
parent | c34d25e011402aedad62b3fe9b7b04989df4522e (diff) | |
download | compcert-kvx-2dd133f9178ae285d3939f29479b4acd9dad394d.tar.gz compcert-kvx-2dd133f9178ae285d3939f29479b4acd9dad394d.zip |
Update the vendored Flocq library to version 3.4.2
For compatibility with the upcoming Coq 8.14.
Diffstat (limited to 'flocq/IEEE754/Bits.v')
-rw-r--r-- | flocq/IEEE754/Bits.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v index 68bc541a..3c19e31b 100644 --- a/flocq/IEEE754/Bits.v +++ b/flocq/IEEE754/Bits.v @@ -163,11 +163,11 @@ Proof. intros x Hx. unfold split_bits, join_bits. rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak. -pattern x at 4 ; rewrite Z_div_mod_eq_full with x (2^mw)%Z. +pattern x at 4 ; rewrite Z.div_mod with x (2^mw)%Z. apply (f_equal (fun v => (v + _)%Z)). rewrite Zmult_comm. apply f_equal. -pattern (x / (2^mw))%Z at 2 ; rewrite Z_div_mod_eq_full with (x / (2^mw))%Z (2^ew)%Z. +pattern (x / (2^mw))%Z at 2 ; rewrite Z.div_mod with (x / (2^mw))%Z (2^ew)%Z. apply (f_equal (fun v => (v + _)%Z)). replace (x / 2 ^ mw / 2 ^ ew)%Z with (if Zle_bool (2 ^ mw * 2 ^ ew) x then 1 else 0)%Z. case Zle_bool. |