use Z.eqb_eq instead of ?Z.eqb_compare, Zeq_bool_eq (for coq/coq#19801)

PrincetonUniversity · Nov 3, 2024 · 428dbdf · 428dbdf
1 parent 8688af9
commit 428dbdf
Showing 1 changed file with 2 additions and 4 deletions.
diff --git 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)