diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 0e335ad371..5c16ca74c4 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -20,6 +20,8 @@ We define many of the bitvector operations from the
 of SMT-LIBv2.
 -/
 
+set_option linter.missingDocs true
+
 /--
 A bitvector of the specified width.
 
@@ -34,9 +36,9 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated (since := "2024-04-12")]
-protected abbrev Std.BitVec := _root_.BitVec
-
+/--
+Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
+-/
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
 -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index ff75d7028a..53d8bec42a 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -28,6 +28,8 @@ https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
 
 -/
 
+set_option linter.missingDocs true
+
 open Nat Bool
 
 namespace Bool
diff --git a/src/Init/Data/BitVec/Folds.lean b/src/Init/Data/BitVec/Folds.lean
index 603a1f4f7f..3dddf614e0 100644
--- a/src/Init/Data/BitVec/Folds.lean
+++ b/src/Init/Data/BitVec/Folds.lean
@@ -8,6 +8,8 @@ import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate
 
+set_option linter.missingDocs true
+
 namespace BitVec
 
 /--
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 6976d00eba..da1ca96bc9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -12,6 +12,8 @@ import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Int.Bitwise.Lemmas
 
+set_option linter.missingDocs true
+
 namespace BitVec
 
 /--