chore: remove lint disabling

opencompl · Sep 4, 2024 · d30baea · d30baea
1 parent 3a138ad
commit d30baea
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -28,8 +28,6 @@ https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
 
 -/
 
--- temporary disable the missing docs to get CI green during patch development
-set_option linter.unusedVariables false
 set_option linter.missingDocs true
 
 open Nat Bool