chore: replace Std with Batteries and recycle a doc-string (#859)

leanprover-community · Jun 25, 2024 · 93343d4 · 93343d4
1 parent da2d1d4
commit 93343d4
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Batteries/Linter/UnnecessarySeqFocus.lean b/Batteries/Linter/UnnecessarySeqFocus.lean
@@ -7,7 +7,7 @@ import Lean.Elab.Command
 import Lean.Linter.Util
 import Batteries.Lean.AttributeExtra
 
-namespace Std.Linter
+namespace Batteries.Linter
 open Lean Elab Command Linter
 
 /--
@@ -147,7 +147,7 @@ partial def markUsedTactics : InfoTree → M ω Unit
 
 end
 
-/-- The main entry point to the unused tactic linter. -/
+@[inherit_doc Batteries.Linter.linter.unnecessarySeqFocus]
 def unnecessarySeqFocusLinter : Linter where run := withSetOptionIn fun stx => do
   unless getLinterUnnecessarySeqFocus (← getOptions) && (← getInfoState).enabled do
     return