Update the vendored Flocq library to version 3.4.2

For compatibility with the upcoming Coq 8.14.

2 files changed, 4 insertions, 4 deletions

diff --git a/flocq/IEEE754/Binary.v b/flocq/IEEE754/Binary.v
index 35d15cb3..4516f0a0 100644
--- a/flocq/IEEE754/Binary.v
+++ b/flocq/IEEE754/Binary.v
@@ -2472,9 +2472,9 @@ case f.
     now revert Hover; unfold B2R, F2R; simpl; rewrite Rmult_assoc, bpow_plus.
 Qed.
 
-(** This hypothesis is needed to implement Bfrexp
+(** This hypothesis is needed to implement [Bfrexp]
     (otherwise, we have emin > - prec
-     and Bfrexp cannot fit the mantissa in interval [0.5, 1)) *)
+     and [Bfrexp] cannot fit the mantissa in interval #[0.5, 1)#) *)
 Hypothesis Hemax : (3 <= emax)%Z.
 
 Definition Ffrexp_core_binary s m e :=
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.