From 8f5a760b894e977e04e74def6d7b2f549291e3b5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 31 Jul 2015 08:55:14 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): display the whole proof state in option "--goal" see issue #755 --- src/frontends/lean/elaborator.cpp | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 95805a2cb..42009c99a 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1849,17 +1849,10 @@ void elaborator::show_goal(proof_state const & ps, expr const & start, expr cons if (curr_pos->first < line || (curr_pos->first == line && curr_pos->second < col)) return; m_ctx.reset_show_goal_at(); - goals const & gs = ps.get_goals(); auto out = regular(env(), ios()); print_lean_info_header(out.get_stream()); out << "position " << curr_pos->first << ":" << curr_pos->second << "\n"; - if (empty(gs)) { - out << "no goals\n"; - } else { - goal g = head(gs); - g = g.instantiate(ps.get_subst()); - out << g << "\n"; - } + out << ps.pp(env(), ios()) << "\n"; print_lean_info_footer(out.get_stream()); }