diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index 371690c85c..6107de39ec 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -44,12 +44,17 @@ optional<metavar_decl> tactic_state::get_main_goal_decl() const {
     return mctx().get_metavar_decl(head(goals()));
 }
 
-tactic_state mk_tactic_state_for(environment const & env, options const & o, local_context const & lctx, expr const & type) {
-    metavar_context mctx;
+tactic_state mk_tactic_state_for(environment const & env, options const & o, metavar_context mctx,
+                                 local_context const & lctx, expr const & type) {
     expr main = mctx.mk_metavar_decl(lctx, type);
     return tactic_state(env, o, mctx, list<expr>(main), main);
 }
 
+tactic_state mk_tactic_state_for(environment const & env, options const & o, local_context const & lctx, expr const & type) {
+    metavar_context mctx;
+    return mk_tactic_state_for(env, o, mctx, lctx, type);
+}
+
 tactic_state set_options(tactic_state const & s, options const & o) {
     return tactic_state(s.env(), o, s.mctx(), s.goals(), s.main());
 }
diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h
index afea537459..6471f12885 100644
--- a/src/library/tactic/tactic_state.h
+++ b/src/library/tactic/tactic_state.h
@@ -73,7 +73,10 @@ inline optional<tactic_state> none_tactic_state() { return optional<tactic_state
 inline optional<tactic_state> some_tactic_state(tactic_state const & e) { return optional<tactic_state>(e); }
 inline optional<tactic_state> some_tactic_state(tactic_state && e) { return optional<tactic_state>(std::forward<tactic_state>(e)); }
 
-tactic_state mk_tactic_state_for(environment const & env, options const & opts, local_context const & lctx, expr const & type);
+tactic_state mk_tactic_state_for(environment const & env, options const & opts, metavar_context mctx,
+                                 local_context const & lctx, expr const & type);
+tactic_state mk_tactic_state_for(environment const & env, options const & opts,
+                                 local_context const & lctx, expr const & type);
 
 tactic_state set_options(tactic_state const & s, options const & o);
 tactic_state set_env(tactic_state const & s, environment const & env);