From 1cf6659dd698cafad6cf55a724a77ea12598262e Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 11 Aug 2022 14:16:09 +0200
Subject: [PATCH] fix typo

---
 stdpp_unstable/bitblast.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stdpp_unstable/bitblast.v b/stdpp_unstable/bitblast.v
index d8f71e5a..04931c28 100644
--- a/stdpp_unstable/bitblast.v
+++ b/stdpp_unstable/bitblast.v
@@ -9,7 +9,7 @@ From stdpp Require Import options.
 (** * [bitblast] tactic: Solve integer goals by bitwise reasoning *)
 (** This file provides the [bitblast] tactic for bitwise reasoning
 about [Z] via [Z.testbit]. Concretely, [bitblast] first turns an
-equality [a = b] into [∀ n, Z.testbit a n = Z.testbit a b], then
+equality [a = b] into [∀ n, Z.testbit a n = Z.testbit b n], then
 simplifies the [Z.testbit] expressions using lemmas like
 [Z.testbit (Z.land a b) n = Z.testbit a n && Z.testbit b n], or
 [Z.testbit (Z.ones z) n = bool_decide (0 ≤ n < z) || bool_decide (z < 0 ∧ 0 ≤ n)]
-- 
GitLab