From 8d97b7c72e2982ca6e4db440229ea6af586567e0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2020 19:00:56 -0800 Subject: [PATCH] chore: missing `,` --- src/Init/Lean/Meta/Message.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Meta/Message.lean b/src/Init/Lean/Meta/Message.lean index b908e67998..fde90ecc32 100644 --- a/src/Init/Lean/Meta/Message.lean +++ b/src/Init/Lean/Meta/Message.lean @@ -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