From 21735deaa48196f4f47dbcd0d9c847871ca674d9 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 3 Nov 2024 16:28:34 +0000 Subject: [PATCH] use Z.eqb_eq instead of Z.eqb_compare (for coq/coq#19801) --- lib/IEEE754_extra.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index cbb63075e8..2d6e6cf554 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -992,9 +992,7 @@ 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 Z.eqb_eq. rewrite <- Zle_is_le_bool. rewrite Bexact_inverse_mantissa_digits2_pos. unfold fexp, FLT_exp, emin. lia. Qed.