add note for bump to 4.6.0

hhu-adam · Feb 14, 2024 · c40705a · c40705a
1 parent e998b90
commit c40705a
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Game/Modification/Tactic.lean b/Game/Modification/Tactic.lean
@@ -65,6 +65,7 @@ elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+)
   let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved
   g.withContext do
     let elimInfo ← getElimInfo `CustomTactic.rec'
+    -- TODO: in v4.6.0 we'll need to replace `targets` with `targets.1`
     let targets ← addImplicitTargets elimInfo targets
     evalInduction.checkTargets targets
     let targetFVarIds := targets.map (·.fvarId!)