diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 57804e85f2..224028daba 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1738,13 +1738,14 @@ elaborate(environment const & env, options const & opts,
     return p;
 }
 
-expr nested_elaborate(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
+expr nested_elaborate(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
                       expr const & e, bool relaxed) {
     elaborator elab(env, opts, mctx, lctx);
     expr r = elab(translate(env, lctx, e));
     if (!relaxed)
         elab.ensure_no_unassigned_metavars();
     mctx = elab.mctx();
+    env  = elab.env();
     return r;
 }
 
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index dea049d6c3..d880c41074 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -201,13 +201,14 @@ public:
     expr operator()(expr const & e);
     pair<expr, level_param_names> finalize(expr const & e, bool check_unassigned, bool to_simple_metavar);
     void ensure_no_unassigned_metavars();
+    environment const & env() const { return m_env; }
 };
 
 pair<expr, level_param_names> elaborate(environment const & env, options const & opts,
                                         metavar_context & mctx, local_context const & lctx,
                                         expr const & e, bool check_unassigend);
 
-expr nested_elaborate(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
+expr nested_elaborate(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
                       expr const & e, bool relaxed);
 
 void initialize_elaborator();
diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp
index 334d68f3bd..b3b40dabce 100644
--- a/src/library/tactic/elaborate.cpp
+++ b/src/library/tactic/elaborate.cpp
@@ -37,7 +37,8 @@ vm_obj tactic_to_expr_core(vm_obj const & relaxed, vm_obj const & qe, vm_obj con
     }
     metavar_context mctx = s.mctx();
     try {
-        expr r = (*g_elaborate)(s.env(), s.get_options(), mctx, g->get_context(), to_expr(qe), to_bool(relaxed));
+        environment env = s.env();
+        expr r = (*g_elaborate)(env, s.get_options(), mctx, g->get_context(), to_expr(qe), to_bool(relaxed));
         r = mctx.instantiate_mvars(r);
         if (relaxed && has_expr_metavar(r)) {
             buffer<expr> new_goals;
@@ -52,9 +53,9 @@ vm_obj tactic_to_expr_core(vm_obj const & relaxed, vm_obj const & qe, vm_obj con
                     return true;
                 });
             list<expr> new_gs = cons(head(s.goals()), to_list(new_goals.begin(), new_goals.end(), tail(s.goals())));
-            return mk_tactic_success(to_obj(r), set_mctx_goals(s, mctx, new_gs));
+            return mk_tactic_success(to_obj(r), set_env_mctx_goals(s, env, mctx, new_gs));
         } else {
-            return mk_tactic_success(to_obj(r), set_mctx(s, mctx));
+            return mk_tactic_success(to_obj(r), set_env_mctx(s, env, mctx));
         }
     } catch (exception & ex) {
         return mk_tactic_exception(ex, s);
diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h
index 70cd479b6a..fdb63d02d4 100644
--- a/src/library/tactic/elaborate.h
+++ b/src/library/tactic/elaborate.h
@@ -16,7 +16,7 @@ expr const & get_by_arg(expr const & e);
 /* Elaboration function.
    \remark The boolean flag indicates whether metavariables should be tolerated in the result or not.
    \remark The metavariable context is input/output. */
-typedef std::function<expr(environment const &, options const &, metavar_context &, local_context const &, expr const &, bool)> elaborate_fn;
+typedef std::function<expr(environment &, options const &, metavar_context &, local_context const &, expr const &, bool)> elaborate_fn;
 
 /** \brief Auxiliary function for setting the thread local elaboration
     procedure used by the tactic framework. */
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index 34b299371c..8d42c92a1e 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -67,6 +67,10 @@ tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx) {
     return tactic_state(s.env(), s.get_options(), mctx, s.goals(), s.main());
 }
 
+tactic_state set_env_mctx(tactic_state const & s, environment const & env, metavar_context const & mctx) {
+    return tactic_state(env, s.get_options(), mctx, s.goals(), s.main());
+}
+
 static list<expr> consume_solved_prefix(metavar_context const & mctx, list<expr> const & gs) {
     if (empty(gs))
         return gs;
@@ -84,6 +88,11 @@ tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx
     return tactic_state(s.env(), s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main());
 }
 
+tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env,
+                                metavar_context const & mctx, list<expr> const & gs) {
+    return tactic_state(env, s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main());
+}
+
 format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) const {
     type_context ctx = mk_type_context_for(*this, transparency_mode::All);
     formatter fmt = fmtf(env(), get_options(), ctx);
diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h
index ad58667a7f..3f9ff63d25 100644
--- a/src/library/tactic/tactic_state.h
+++ b/src/library/tactic/tactic_state.h
@@ -81,8 +81,10 @@ tactic_state mk_tactic_state_for(environment const & env, options const & opts,
 tactic_state set_options(tactic_state const & s, options const & o);
 tactic_state set_env(tactic_state const & s, environment const & env);
 tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx);
+tactic_state set_env_mctx(tactic_state const & s, environment const & env, metavar_context const & mctx);
 tactic_state set_goals(tactic_state const & s, list<expr> const & gs);
 tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list<expr> const & gs);
+tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env, metavar_context const & mctx, list<expr> const & gs);
 
 tactic_state const & to_tactic_state(vm_obj const & o);
 vm_obj to_obj(tactic_state const & s);