From 91f83835bbf139417bbf17dc502ee6e93f4f8c29 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jul 2015 20:11:27 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): "show goal" command line option for nested "begin...end" blocks --- 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 9ee620a49..fd07d5063 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1857,7 +1857,6 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr buffer pre_tac_seq; extract_begin_end_tactics(get_annotation_arg(pre_tac), pre_tac_seq); for (expr ptac : pre_tac_seq) { - show_goal(ps, pre_tac, ptac); if (is_begin_end_annotation(ptac)) { goals gs = ps.get_goals(); if (!gs) @@ -1870,6 +1869,7 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr return false; ps = proof_state(ps, tail(gs), subst, ngen); } else { + show_goal(ps, pre_tac, ptac); expr new_ptac = subst.instantiate_all(ptac); if (auto tac = pre_tactic_to_tactic(new_ptac)) { try {