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

perf(kernel/error_msgs): avoid unnecessary work

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-15 18:32:27 -08:00
parent ce0b1d17a2
commit f397da111a
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/error_msgs.cpp
View file

@ -31,7 +31,9 @@ list<options> set_distinguishing_pp_options(list<options> const & opts) {
static expr erase_binder_info(expr const & e) {
return replace(e, [](expr const & e) {
if (is_binding(e) && binding_info(e) != binder_info()) {
if (is_local(e) || is_metavar(e)) {
return some_expr(e);
} else if (is_binding(e) && binding_info(e) != binder_info()) {
return some_expr(update_binding(e, erase_binder_info(binding_domain(e)),
erase_binder_info(binding_body(e)), binder_info()));
} else {