From c11bcdc2fdbe8ddaa43ac8ff6a43af86d6406d3a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 25 Sep 2016 12:52:58 -0700 Subject: [PATCH] fix(library/type_context): incorrect context being used when tracing type classes resolution --- src/library/type_context.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 526cf0c747..83897b8e5a 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -2690,7 +2690,9 @@ struct instance_synthesizer { r = mk_app(r, new_arg); type = instantiate(binding_body(type), new_arg); } - lean_trace_plain("class_instances", trace(e.m_depth, mk_app(mvar, locals.as_buffer()), mvar_type, r);); + lean_trace_plain("class_instances", + scope_trace_env scope(m_ctx.env(), m_ctx); + trace(e.m_depth, mk_app(mvar, locals.as_buffer()), mvar_type, r);); if (!m_ctx.is_def_eq(mvar_type, type)) { return false; }