fix

Rob23oba · Rob23oba · commit b1c001d74c07 · 2025-06-11T19:23:09.000+02:00
diff --git a/Batteries/Linter/UnnecessarySeqFocus.lean b/Batteries/Linter/UnnecessarySeqFocus.lean
@@ -67,7 +67,7 @@ initialize multigoalAttr : TagAttributeExtra ←
     ``Parser.Tactic.Conv.case',
     ``Parser.Tactic.rotateLeft,
     ``Parser.Tactic.rotateRight,
-    ``Parser.Tactic.tacticShow_,
+    ``Parser.Tactic.show,
     ``Parser.Tactic.tacticStop_
   ]
 

Original file line number	Diff line number	Diff line change
`@@ -67,7 +67,7 @@ initialize multigoalAttr : TagAttributeExtra ←`
`67`	`67`	``Parser.Tactic.Conv.case',
`68`	`68`	``Parser.Tactic.rotateLeft,
`69`	`69`	``Parser.Tactic.rotateRight,
`70`		- ``Parser.Tactic.tacticShow_,
	`70`	+ ``Parser.Tactic.show,
`71`	`71`	``Parser.Tactic.tacticStop_
`72`	`72`	`]`
`73`	`73`