From ccd7af00083eb8927e8854870b78dffa30a1df7c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Jan 2020 20:25:22 -0800
Subject: [PATCH] feat: display unsolved goals

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

diff --git a/src/Init/Lean/Elab/Tactic.lean b/src/Init/Lean/Elab/Tactic.lean
index 1b5cc14d60..871761281c 100644
--- a/src/Init/Lean/Elab/Tactic.lean
+++ b/src/Init/Lean/Elab/Tactic.lean
@@ -33,8 +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 :=
--- TODO: pretty print goals
-throwError ref "there are unsolved goals"
+throwError ref $ "unsolved goals" ++ Format.line ++ MessageData.joinSep (goals.map $ MessageData.ofGoal) Format.line
 
 def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
 modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s };