diff options
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 0ce214bbd..7158dc22a 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -1230,7 +1230,6 @@ Section Conversion. /\ Z.of_nat i <= bitsIn limb_widthsA /\ forall n, Z.testbit (decodeB out) n = if Z_lt_dec n (Z.of_nat i) then Z.testbit (decodeA inp) n else false. - Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end. Ltac subst_lia := subst_let; subst; lia. Lemma convert'_bounded_step : forall inp i out, |