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

chore(library/blast/state): do not display set of active hypotheses

Browse source 
This is just "noise" in error messages
This commit is contained in:
Leonardo de Moura 2015-12-30 11:31:59 -08:00
parent dc6a3e30c0
commit 2a454ce791
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/blast/state.cpp
View file

@ -297,7 +297,6 @@ void state::display(environment const & env, io_state const & ios) const {
formatter fmt = ios.get_formatter_factory()(env, ios.get_options());
auto & out = ios.get_diagnostic_channel();
out << mk_pair(to_goal().pp(fmt), ios.get_options()) << "\n";
display_active(out.get_stream());
}
bool state::has_assigned_uref(level const & l) const {