Adapt to coq/coq#19530 (#524)

Splitting coq-stdlib out introduces a mysterious problem with `Zeq_bool`. This PR is a work around.
AbsInt · Oct 3, 2024 · 5f90f91 · 5f90f91
1 parent 1eb3496
commit 5f90f91
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/lib/IEEE754_extra.v b/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.