diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index c3d20a5bb1..3b7fa3b622 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1312,6 +1312,7 @@ expr elaborator::visit_equations(expr const & e) {
     new_e = instantiate_mvars(new_e);
     metavar_context mctx = m_ctx.mctx();
     expr r = compile_equations(m_env, m_opts, mctx, m_ctx.lctx(), new_e);
+    m_ctx.set_env(m_env);
     m_ctx.set_mctx(mctx);
     return r;
 }
@@ -1658,6 +1659,7 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
         }
         mctx.assign(mvar, val);
         m_env = new_s->env();
+        m_ctx.set_env(m_env);
         m_ctx.set_mctx(mctx);
     } else if (optional<pair<format, tactic_state>> ex = is_tactic_exception(S, m_opts, r)) {
         throw_unsolved_tactic_state(ex->second, ex->first, ref);
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index e8e26ce38d..d7baa196da 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -217,6 +217,16 @@ type_context::~type_context() {
         m_cache_manager->recycle(m_cache);
 }
 
+void type_context::set_env(environment const & env) {
+    options o = m_cache->m_options;
+    if (m_cache_manager) {
+        m_cache_manager->recycle(m_cache);
+        m_cache = m_cache_manager->mk(env, o);
+    } else {
+        m_cache = mk_cache(env, o, false);
+    }
+}
+
 expr type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {
     return m_lctx.mk_local_decl(pp_name, type, bi);
 }
diff --git a/src/library/type_context.h b/src/library/type_context.h
index f9513c34a1..9b5d300edc 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -235,8 +235,10 @@ public:
     expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
     level mk_univ_metavar_decl() { return m_mctx.mk_univ_metavar_decl(); }
 
-    /* note: mctx must be a descendent of m_mctx */
+    /* note: mctx must be a descendant of m_mctx */
     void set_mctx(metavar_context const & mctx) { m_mctx = mctx; }
+    /* note: env must be a descendant of m_env */
+    void set_env(environment const & env);
 
     bool is_def_eq_core(level const & l1, level const & l2);
     bool is_def_eq(level const & l1, level const & l2);