From 8688af9f9f08d2898c833ef681cf4a0d1aa1d485 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 19 Sep 2024 16:33:08 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 (#794)

---
 compcert/lib/IEEE754_extra.v | 2 ++
 progs/verif_union.v          | 2 ++
 progs64/verif_union.v        | 2 ++
 3 files changed, 6 insertions(+)

diff --git a/compcert/lib/IEEE754_extra.v b/compcert/lib/IEEE754_extra.v
index f7c2487b9..cbb63075e 100644
--- a/compcert/lib/IEEE754_extra.v
+++ b/compcert/lib/IEEE754_extra.v
@@ -992,6 +992,8 @@ Remark bounded_Bexact_inverse:
   emin <= e <= emax - prec <-> bounded prec emax Bexact_inverse_mantissa e = true.
 Proof.
   intros. unfold bounded, canonical_mantissa. rewrite andb_true_iff.
+  rewrite ?Z.eqb_compare.
+  fold (Zeq_bool (fexp (Z.pos (digits2_pos Bexact_inverse_mantissa) + e)) e).
   rewrite <- Zeq_is_eq_bool. rewrite <- Zle_is_le_bool.
   rewrite Bexact_inverse_mantissa_digits2_pos.
   unfold fexp, FLT_exp, emin. lia.
diff --git a/progs/verif_union.v b/progs/verif_union.v
index e9af570bc..17395bb0b 100644
--- a/progs/verif_union.v
+++ b/progs/verif_union.v
@@ -145,6 +145,7 @@ rewrite andb_true_iff in H.
 destruct H as [H H0].
 apply Z.leb_le in H0.
 unfold SpecFloat.canonical_mantissa in H.
+rewrite ?Z.eqb_compare in H.
 apply Zeq_bool_eq in H.
 unfold FLT.FLT_exp in H.
 rewrite Digits.Zpos_digits2_pos in H.
@@ -219,6 +220,7 @@ destruct e0 as [H' ?H].
 assert (-149 <= e). {
  clear - H'.
  unfold SpecFloat.canonical_mantissa in H'.
+rewrite ?Z.eqb_compare in H'.
 apply Zeq_bool_eq in H'.
 unfold FLT.FLT_exp in H'.
 rewrite Digits.Zpos_digits2_pos in H'.
diff --git a/progs64/verif_union.v b/progs64/verif_union.v
index cf371d09d..ae8367ae8 100644
--- a/progs64/verif_union.v
+++ b/progs64/verif_union.v
@@ -146,6 +146,7 @@ rewrite andb_true_iff in H.
 destruct H as [H H0].
 apply Z.leb_le in H0.
 unfold SpecFloat.canonical_mantissa in H.
+rewrite ?Z.eqb_compare in H.
 apply Zeq_bool_eq in H.
 unfold FLT.FLT_exp in H.
 rewrite Digits.Zpos_digits2_pos in H.
@@ -220,6 +221,7 @@ destruct e0 as [H' ?H].
 assert (-149 <= e). {
  clear - H'.
  unfold SpecFloat.canonical_mantissa in H'.
+rewrite ?Z.eqb_compare in H'.
 apply Zeq_bool_eq in H'.
 unfold FLT.FLT_exp in H'.
 rewrite Digits.Zpos_digits2_pos in H'.