chore: remove unneeded Batteries reference in repeat doc-string

2026-03-17 18:34:06 +00:00 · 2024-06-04 10:46:42 +10:00
1 changed files with 2 additions and 1 deletions
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -835,7 +835,8 @@ syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic
 /--
 `repeat tac` repeatedly applies `tac` to the main goal until it fails.
 That is, if `tac` produces multiple subgoals, only subgoals up to the first failure will be visited.
-The `Batteries` library provides `repeat'` which repeats separately in each subgoal.
+
+See also the tactic `repeat'` which repeats separately in each subgoal.
 -/
 syntax "repeat " tacticSeq : tactic
 macro_rules