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

feat(library/tactic/proof_state): add empty line between goals, closes #281

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-29 15:55:07 -07:00
parent b0a7888346
commit 95e843e8ed
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/library/tactic/proof_state.cpp
View file

@ -47,7 +47,7 @@ format proof_state::pp(formatter const & fmt) const {
bool first = true;
for (auto const & g : get_goals()) {
if (first) first = false; else r += line();
if (first) first = false; else r += line() + line();
if (show_goal_names) {
r += group(format(g.get_name()) + colon() + nest(indent, line() + g.pp(fmt, m_subst)));
} else {