From 5f90f91a03c5c532e2ae87e4f25c862a6f892743 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Oct 2024 18:58:45 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 (#524) Splitting coq-stdlib out introduces a mysterious problem with `Zeq_bool`. This PR is a work around. --- lib/IEEE754_extra.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index f7c2487b93..cbb63075e8 100644 --- 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.