michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/elaborator): "show goal" command line option for nested "begin...end" blocks

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-27 20:11:27 -07:00
parent a3b570c852
commit 91f83835bb
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -1857,7 +1857,6 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
buffer<expr> 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 {