max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(frontends/lean/old_elaborator): improve error message

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-14 21:47:29 -07:00
parent 5b8ac6ba30
commit 6a22c0f771
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/old_elaborator.cpp
View file

@ -1876,7 +1876,7 @@ void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_sta
flycheck_error err(ios());
if (!err.enabled() || save_error(pip(), pos)) {
display_error_pos(out.get_stream(), out.get_options(), pip(), pos);
out << " " << fmt << "\n" << ts.pp(ios().get_formatter_factory()) << endl;
out << " " << fmt << "\ntactic state:\n" << ts.pp(ios().get_formatter_factory()) << endl;
}
}
}