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

chore: missing ,

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-09 19:00:56 -08:00
parent 55074b2a17
commit 8d97b7c72e
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/Init/Lean/Meta/Message.lean
View file

@ -78,7 +78,7 @@ 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 => mkCtx ctx $ "tactic '" ++ tacName ++ "' failed " ++ msg ++ Format.line ++ MessageData.ofGoal mvarId
| tactic tacName mvarId msg ctx => mkCtx ctx $ "tactic '" ++ tacName ++ "' failed, " ++ msg ++ Format.line ++ MessageData.ofGoal mvarId
| bug _ _ => "internal bug" -- TODO improve
| other s => s