From 662345e2af2b122fedb7c9aa2be2ac454c4bebe2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Aug 2014 18:16:53 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): missing '\n' in error message Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 769245f05..b4f1233b0 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1079,7 +1079,7 @@ public: std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, s.instantiate(t), s.instantiate(v_type)); format r("type mismatch at term"); r += pp_indent_expr(fmt, s.instantiate(v)); - r += format("has type"); + r += compose(line(), format("has type")); r += given_fmt; r += compose(line(), format("but is expected to have type")); r += expected_fmt;