From 428dbdf7a92214ca1666cd4cd9b6a38e604fd4a6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 3 Nov 2024 16:35:22 +0000 Subject: [PATCH] use Z.eqb_eq instead of ?Z.eqb_compare, Zeq_bool_eq (for coq/coq#19801) --- progs/verif_union.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/progs/verif_union.v b/progs/verif_union.v index 17395bb0b..ff476134b 100644 --- a/progs/verif_union.v +++ b/progs/verif_union.v @@ -145,8 +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. +apply Z.eqb_eq in H. unfold FLT.FLT_exp in H. rewrite Digits.Zpos_digits2_pos in H. pose proof (Z.max_lub_l (Digits.Zdigits Zaux.radix2 (Z.pos m) + e - prec) @@ -220,8 +219,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'. +apply Z.eqb_eq in H'. unfold FLT.FLT_exp in H'. rewrite Digits.Zpos_digits2_pos in H'. pose proof (Z.max_lub_r (Digits.Zdigits Zaux.radix2 (Z.pos m) + e - 24)