From d75bd2ae98bfbb6cf774c09a8a980d79e82c331a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 24 Nov 2013 20:22:47 -0800
Subject: [PATCH] feat(library/tactic/proof_state): remove goal name when
 pretty printing the proof state

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/proof_state.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index af4397b822..e6d09b5e18 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/src/library/tactic/proof_state.cpp
@@ -16,7 +16,7 @@ format proof_state::pp(formatter const & fmt, options const & opts) const {
             first = false;
         else
             r += line();
-        r += group(format{format(p.first), colon(), line(), p.second.pp(fmt, opts)});
+        r += p.second.pp(fmt, opts);
     }
     return r;
 }