# --- T2-COPYRIGHT-BEGIN ---
# t2/package/*/compcert/fix-mantissa-rewrite.patch
# Copyright (C) 2025 The T2 SDE Project
# SPDX-License-Identifier: GPL-2.0 or patched project license
# --- T2-COPYRIGHT-END ---

--- CompCert-3.15/lib/IEEE754_extra.v.vanilla	2024-12-13 11:06:04.000000000 +0100
+++ CompCert-3.15/lib/IEEE754_extra.v	2025-07-21 18:42:22.865072246 +0200
@@ -992,8 +992,6 @@
   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.