From c32138db88ff4a4e2a244729a0c96a1dcbee00dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Aug 2016 15:32:04 -0700 Subject: [PATCH] feat(library/type_context): add new trace msg --- src/library/type_context.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 80f02014a3..3cdd378944 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1461,6 +1461,10 @@ optional type_context::check_assignment(buffer const & locals, expr if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) { return mlocal_name(a) != mlocal_name(e); })) { ok = false; + lean_trace(name({"type_context", "is_def_eq_detail"}), + tout() << "failed to assign " << mvar << " to\n" << v << "\n" << + "value contains local declaration " << e << + " which is not in the scope of the metavariable";); return false; } }