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

chore(tactic/simplifier/simplifier): remove old todos

Browse source
This commit is contained in:
Daniel Selsam 2016-07-03 02:50:32 +01:00 • committed by Leonardo de Moura
parent f03df9196b
commit d3cfd39278
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/simplifier/simplifier.cpp
View file

@ -463,12 +463,10 @@ simp_result simplifier::simplify_extensions(expr const & _e) {
} else {
lean_trace(name({"simplifier", "extensions"}),
tout() << "extension succeeded but left metavariables unassigned\n";);
// TODO(dhs): trace "simplifier.extension.failure"
}
} else {
lean_trace(name({"simplifier", "extensions"}),
tout() << "extension failed\n";);
// TODO(dhs): trace "simplifier.extension.failure"
}
}
return r;