max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: missing withTacticInfoContext (#3822)

Browse source 
closes #3720
This commit is contained in:
Leonardo de Moura 2024-04-01 19:15:38 -07:00 • committed by GitHub
parent f35fc18c88
commit 2dab6939e4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/Induction.lean
View file

@ -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