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

fix: display goal at error

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-16 19:32:58 -08:00
parent 72c6194d9b
commit f6622b3120
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Meta/Exception.lean
View file

@ -92,9 +92,7 @@ def toTraceMessageData : Exception → MessageData
| notInstance i ctx => mkCtx ctx $ `notInstance ++ " " ++ i
| appBuilder op msg args ctx => mkCtx ctx $ `appBuilder ++ " " ++ op ++ " " ++ args ++ " " ++ msg
| synthInstance inst ctx => mkCtx ctx $ `synthInstance ++ " " ++ inst
| tactic tacName mvarId msg ctx =>
mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg ++ Format.line ++
ppGoal ctx.env ctx.mctx ctx.lctx ctx.opts mvarId
| tactic tacName mvarId msg ctx => mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg
| bug _ _ => "internal bug" -- TODO improve
| other s => s

4
src/Init/Lean/Meta/Message.lean
View file

@ -78,7 +78,9 @@ def toMessageData : Exception → MessageData
| notInstance i ctx => mkCtx ctx $ "not a type class instance " ++ i
| appBuilder op msg args ctx => mkCtx ctx $ "application builder failure " ++ op ++ " " ++ args ++ " " ++ msg
| synthInstance inst ctx => mkCtx ctx $ "failed to synthesize" ++ indentExpr inst
| tactic tacName mvarId msg ctx => "tactic '" ++ tacName ++ "' failed " ++ msg
| tactic tacName mvarId msg ctx =>
"tactic '" ++ tacName ++ "' failed " ++ msg ++ Format.line ++
ppGoal ctx.env ctx.mctx ctx.lctx ctx.opts mvarId
| bug _ _ => "internal bug" -- TODO improve
| other s => s