From 20210928da4b7fd9e79ae8aeeb86b81f5dd30fc2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 Jul 2020 11:18:28 -0700 Subject: [PATCH] fix: missing line breaks --- src/Lean/Message.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index b0e984013d..2d853ce6bf 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -207,8 +207,8 @@ match e with | appTypeMismatch env lctx e fnType argType => mkCtx env lctx opts $ "application type mismatch" ++ indentExpr e - ++ "argument has type" ++ indentExpr argType - ++ "but function has type" ++ indentExpr fnType + ++ Format.line ++ "argument has type" ++ indentExpr argType + ++ Format.line ++ "but function has type" ++ indentExpr fnType | invalidProj env lctx e => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e | other msg => "(kernel) " ++ msg