From f397da111a97b458601a10d673c93d7e814ebe9e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Jan 2015 18:32:27 -0800 Subject: [PATCH] perf(kernel/error_msgs): avoid unnecessary work --- src/kernel/error_msgs.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index 9031dce0c..2abf4e64a 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -31,7 +31,9 @@ list set_distinguishing_pp_options(list 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 {