From fed91dcbfaa14fc849ef5f6f59e6acfb19da162d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jan 2020 16:47:08 -0800
Subject: [PATCH] chore: add line break between goals

---
 src/Init/Lean/Elab/Tactic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/Tactic.lean b/src/Init/Lean/Elab/Tactic.lean
index 6616b75604..c08cf2b4c4 100644
--- a/src/Init/Lean/Elab/Tactic.lean
+++ b/src/Init/Lean/Elab/Tactic.lean
@@ -33,7 +33,7 @@ withMVarContext mvarId $ fun ctx s =>
   | EStateM.Result.ok a newS     => EStateM.Result.ok a newS.toTermState
 
 def reportUnsolvedGoals (ref : Syntax) (goals : List MVarId) : TermElabM Unit :=
-throwError ref $ "unsolved goals" ++ Format.line ++ MessageData.joinSep (goals.map $ MessageData.ofGoal) Format.line
+throwError ref $ "unsolved goals" ++ Format.line ++ MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
 
 def ensureAssignmentHasNoMVars (ref : Syntax) (mvarId : MVarId) : TermElabM Unit := do
 val ← instantiateMVars ref (mkMVar mvarId);