From 0261cb95bf3f4296a33cca599fc09f355fb7b047 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jun 2016 11:09:14 -0700 Subject: [PATCH] feat(frontends/lean/old_elaborator): use type_context for failure tactic_state --- src/frontends/lean/old_elaborator.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index d61142caf6..08710c36b7 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -1872,7 +1872,9 @@ void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_sta lean_assert(is_metavar(mvar)); if (!m_displayed_errors.contains(mlocal_name(mvar))) { m_displayed_errors.insert(mlocal_name(mvar)); - auto out = regular(env(), ios(), m_tc->get_type_context()); + metavar_context mctx = ts.mctx(); + type_context ctx = mk_type_context_for(ts, mctx); + auto out = regular(env(), ios(), ctx); flycheck_error err(ios()); if (!err.enabled() || save_error(pip(), pos)) { display_error_pos(out.get_stream(), out.get_options(), pip(), pos);