From ec141d1671ffe9a20cba42d763cc148eec8b79d4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Feb 2018 10:35:14 -0800 Subject: [PATCH] chore(library/tactic/change_tactic): use type_context instead of metavar_context --- src/library/tactic/change_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp index 31aebe2d5a..c8d9a6ac12 100644 --- a/src/library/tactic/change_tactic.cpp +++ b/src/library/tactic/change_tactic.cpp @@ -18,9 +18,8 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) { if (e == g->get_type()) return tactic::mk_success(s); type_context ctx = mk_type_context_for(s); if (!check || ctx.is_def_eq(e, g->get_type())) { - auto mctx = ctx.mctx(); - expr new_e = mctx.instantiate_mvars(e); - expr new_M = mctx.mk_metavar_decl(g->get_context(), new_e); + expr new_e = ctx.instantiate_mvars(e); + expr new_M = ctx.mk_metavar_decl(g->get_context(), new_e); /* We use the proof term @@ -29,6 +28,7 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) { to create a "checkpoint". See discussion at issue #1260 */ expr pr = mk_id(ctx, g->get_type(), new_M); + auto mctx = ctx.mctx(); mctx.assign(head(s.goals()), pr); list new_gs(new_M, tail(s.goals())); return tactic::mk_success(set_mctx_goals(s, mctx, new_gs));