fix: missing withTacticInfoContext

2026-03-29 16:24:08 +00:00 · 2024-04-01 18:57:24 -07:00
1 changed files with 1 additions and 1 deletions
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -59,7 +59,7 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) (remaini
  withCaseRef (getAltDArrow alt) rhs do
    if isHoleRHS rhs then
      addInfo
-      let gs' ← mvarId.withContext <| withRef rhs do
+      let gs' ← mvarId.withContext <| withTacticInfoContext rhs do
        let mvarDecl ← mvarId.getDecl
        let val ← elabTermEnsuringType rhs mvarDecl.type
        mvarId.assign val