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

fix: use correct metavar context

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-23 05:15:36 -07:00
parent 630dcf4cc1
commit de4bede6ff
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Term.lean
View file

@ -370,7 +370,7 @@ def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit := d
msg ++ " " ++ arg.getAppFn
else
msg ++ " …"
let msg : MessageData := "don't know how to synthesize implicit argument" ++ indentD msg
let msg : MessageData := msg!"don't know how to synthesize implicit argument{indentD msg}"
let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId
logErrorAt mvarErrorInfo.ref msg
| MVarErrorKind.hole => do
@ -392,7 +392,7 @@ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) : TermElabM Boo
let mvarId := mvarErrorInfo.mvarId;
if alreadyVisited.contains mvarId then
pure (foundErrors, alreadyVisited)
else do
else withMVarContext mvarId do
let alreadyVisited := alreadyVisited.insert mvarId
/- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
delayed assigned to another metavariable that is unassigned. -/