From b19278e604f1cae2cb6343e41cf4bb73fcaefcc4 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 9 Jan 2025 08:09:20 -0500 Subject: [PATCH] Revert "Adapt to https://github.com/coq/coq/pull/19530 (#794)" (#799) This reverts commit 8688af9f9f08d2898c833ef681cf4a0d1aa1d485. --- compcert/lib/IEEE754_extra.v | 2 -- progs/verif_union.v | 2 -- progs64/verif_union.v | 2 -- 3 files changed, 6 deletions(-) diff --git a/compcert/lib/IEEE754_extra.v b/compcert/lib/IEEE754_extra.v index cbb63075e..f7c2487b9 100644 --- a/compcert/lib/IEEE754_extra.v +++ b/compcert/lib/IEEE754_extra.v @@ -992,8 +992,6 @@ 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. diff --git a/progs/verif_union.v b/progs/verif_union.v index 17395bb0b..e9af570bc 100644 --- a/progs/verif_union.v +++ b/progs/verif_union.v @@ -145,7 +145,6 @@ 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. unfold FLT.FLT_exp in H. rewrite Digits.Zpos_digits2_pos in H. @@ -220,7 +219,6 @@ 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'. unfold FLT.FLT_exp in H'. rewrite Digits.Zpos_digits2_pos in H'. diff --git a/progs64/verif_union.v b/progs64/verif_union.v index ae8367ae8..cf371d09d 100644 --- a/progs64/verif_union.v +++ b/progs64/verif_union.v @@ -146,7 +146,6 @@ 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. unfold FLT.FLT_exp in H. rewrite Digits.Zpos_digits2_pos in H. @@ -221,7 +220,6 @@ 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'. unfold FLT.FLT_exp in H'. rewrite Digits.Zpos_digits2_pos in H'.