diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 4f7e5d18ea..4a8bb34f30 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2681,7 +2681,7 @@ expr elaborator::visit_equations(expr const & e) {
     new_e = instantiate_mvars(new_e);
     ensure_no_unassigned_metavars(new_e);
     metavar_context mctx = m_ctx.mctx();
-    expr r = compile_equations(m_env, m_opts, mctx, m_ctx.lctx(), new_e, *this);
+    expr r = compile_equations(m_env, *this, mctx, m_ctx.lctx(), new_e);
     m_ctx.set_env(m_env);
     m_ctx.set_mctx(mctx);
     return r;
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index d9eedd288b..f3daa45643 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -296,8 +296,16 @@ public:
                metavar_context const & mctx, local_context const & lctx,
                bool recover_from_errors = true, bool in_pattern = false, bool in_quote = false);
     ~elaborator();
+    abstract_context_cache & get_cache() { return m_cache; }
     metavar_context const & mctx() const { return m_ctx.mctx(); }
     local_context const & lctx() const { return m_ctx.lctx(); }
+    environment const & env() const { return m_env; }
+    options const & get_options() const { return m_opts; }
+    void set_env(environment const & env) {
+        m_env = env;
+        m_ctx.set_env(m_env);
+    }
+
     expr push_local(name const & n, expr const & type, binder_info const & bi = binder_info()) {
         return m_ctx.push_local(n, type, bi);
     }
@@ -337,12 +345,6 @@ public:
     pair<expr, theorem_finalization_info> finalize_theorem_type(expr const & type, buffer<name> & new_lp_names);
     expr finalize_theorem_proof(expr const & val, theorem_finalization_info const & info);
 
-    environment const & env() const { return m_env; }
-    void set_env(environment const & env) {
-        m_env = env;
-        m_ctx.set_env(m_env);
-    }
-
     bool has_errors() const { return m_has_errors; }
 };
 
diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp
index 772a62dbfe..771dc0fc51 100644
--- a/src/library/equations_compiler/compiler.cpp
+++ b/src/library/equations_compiler/compiler.cpp
@@ -29,10 +29,8 @@ static bool has_nested_rec(expr const & eqns) {
             }));
 }
 
-static eqn_compiler_result compile_equations_core(environment & env, options const & opts,
-                                   metavar_context & mctx, local_context const & lctx,
-                                   expr const & eqns, elaborator & elab) {
-    type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
+static eqn_compiler_result compile_equations_core(environment & env, elaborator & elab, metavar_context & mctx, local_context const & lctx, expr const & eqns) {
+    type_context ctx(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
     trace_compiler(tout() << "compiling\n" << eqns << "\n";);
     trace_compiler(tout() << "recursive:          " << is_recursive_eqns(ctx, eqns) << "\n";);
     trace_compiler(tout() << "nested recursion:   " << has_nested_rec(eqns) << "\n";);
@@ -44,22 +42,22 @@ static eqn_compiler_result compile_equations_core(environment & env, options con
         if (is_wf_equations(eqns)) {
             throw exception("invalid use of 'using_well_founded', we do not need to use well founded recursion for meta definitions, since they can use unbounded recursion");
         }
-        return unbounded_rec(env, opts, mctx, lctx, eqns, elab);
+        return unbounded_rec(env, elab, mctx, lctx, eqns);
     }
 
     if (is_wf_equations(eqns)) {
-        return wf_rec(env, opts, mctx, lctx, eqns, elab);
+        return wf_rec(env, elab, mctx, lctx, eqns);
     }
 
     if (header.m_num_fns == 1) {
         if (!is_recursive_eqns(ctx, eqns)) {
-            return mk_nonrec(env, opts, mctx, lctx, eqns, elab);
-        } else if (auto r = try_structural_rec(env, opts, mctx, lctx, eqns, elab)) {
+            return mk_nonrec(env, elab, mctx, lctx, eqns);
+        } else if (auto r = try_structural_rec(env, elab, mctx, lctx, eqns)) {
             return *r;
         }
     }
 
-    return wf_rec(env, opts, mctx, lctx, eqns, elab);
+    return wf_rec(env, elab, mctx, lctx, eqns);
 }
 
 /** Auxiliary class for pulling nested recursive calls.
@@ -89,15 +87,15 @@ static eqn_compiler_result compile_equations_core(environment & env, options con
     Compile the match, and then beta-reduce.
 */
 struct pull_nested_rec_fn : public replace_visitor {
-    environment &         m_env;
-    options               m_opts;
-    metavar_context &     m_mctx;
-    buffer<local_context> m_lctx_stack;
-    buffer<expr>          m_new_locals;
-    buffer<expr>          m_new_values;
+    environment &            m_env;
+    elaborator &             m_elab;
+    metavar_context &        m_mctx;
+    buffer<local_context>    m_lctx_stack;
+    buffer<expr>             m_new_locals;
+    buffer<expr>             m_new_values;
 
-    pull_nested_rec_fn(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx):
-        m_env(env), m_opts(opts), m_mctx(mctx) {
+    pull_nested_rec_fn(environment & env, elaborator & elab, metavar_context & mctx, local_context const & lctx):
+        m_env(env), m_elab(elab), m_mctx(mctx) {
         m_lctx_stack.push_back(lctx);
     }
 
@@ -106,7 +104,7 @@ struct pull_nested_rec_fn : public replace_visitor {
     local_context & lctx() { return m_lctx_stack.back(); }
 
     type_context mk_type_context(local_context const & lctx) {
-        return type_context(m_env, m_opts, m_mctx, lctx, transparency_mode::Semireducible);
+        return type_context(m_env, m_mctx, lctx, m_elab.get_cache(), transparency_mode::Semireducible);
     }
 
     expr visit_lambda_pi_let(bool is_lam, expr const & e) {
@@ -296,11 +294,11 @@ struct pull_nested_rec_fn : public replace_visitor {
         }
     }
 
-    eqn_compiler_result operator()(expr const & e, elaborator & elab) {
+    eqn_compiler_result operator()(expr const & e) {
         expr new_e             = visit(e);
         lean_assert(m_lctx_stack.size() == 1);
         local_context new_lctx = m_lctx_stack[0];
-        auto r                 = compile_equations_core(m_env, m_opts, m_mctx, new_lctx, new_e, elab);
+        auto r                 = compile_equations_core(m_env, m_elab, m_mctx, new_lctx, new_e);
         type_context ctx       = mk_type_context(new_lctx);
         r.m_fns = map(r.m_fns, [&] (expr const & fn) { return replace_locals(fn, m_new_locals, m_new_values); });
         m_mctx                 = ctx.mctx();
@@ -321,19 +319,19 @@ static expr remove_aux_main_name(expr const & e) {
     return e;
 }
 
-static expr compile_equations_main(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
-                                   expr const & _eqns, elaborator & elab, bool report_cexs) {
+static expr compile_equations_main(environment & env, elaborator & elab,
+                                   metavar_context & mctx, local_context const & lctx, expr const & _eqns, bool report_cexs) {
     expr eqns = _eqns;
     equations_header const & header = get_equations_header(eqns);
     eqn_compiler_result r;
     if (!header.m_is_meta && has_nested_rec(eqns)) {
-        r = pull_nested_rec_fn(env, opts, mctx, lctx)(eqns, elab);
+        r = pull_nested_rec_fn(env, elab, mctx, lctx)(eqns);
     } else {
-        r = compile_equations_core(env, opts, mctx, lctx, eqns, elab);
+        r = compile_equations_core(env, elab, mctx, lctx, eqns);
     }
 
     if (report_cexs && r.m_counter_examples) {
-        auto pp = mk_pp_ctx(env, opts, mctx, lctx);
+        auto pp = mk_pp_ctx(env, elab.get_options(), mctx, lctx);
         auto fmt = format("non-exhaustive match, the following cases are missing:");
         for (auto & ce : r.m_counter_examples) {
             fmt += line() + pp(remove_aux_main_name(ce));
@@ -345,10 +343,9 @@ static expr compile_equations_main(environment & env, options const & opts, meta
     return mk_equations_result(fns.size(), fns.data());
 }
 
-expr compile_equations(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
-                       expr const & eqns, elaborator & elab) {
+expr compile_equations(environment & env, elaborator & elab, metavar_context & mctx, local_context const & lctx, expr const & eqns) {
     equations_header const & header = get_equations_header(eqns);
-    type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
+    type_context ctx(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
     if (!header.m_is_meta &&
         !header.m_is_lemma &&
         !header.m_is_noncomputable &&
@@ -364,9 +361,9 @@ expr compile_equations(environment & env, options const & opts, metavar_context
         aux_header.m_aux_lemmas = false;
         aux_header.m_fn_actual_names = map(header.m_fn_actual_names, mk_aux_meta_rec_name);
         expr aux_eqns = remove_wf_annotation_from_equations(update_equations(eqns, aux_header));
-        compile_equations_main(env, opts, mctx, lctx, aux_eqns, elab, false);
+        compile_equations_main(env, elab, mctx, lctx, aux_eqns, false);
     }
-    return compile_equations_main(env, opts, mctx, lctx, eqns, elab, true);
+    return compile_equations_main(env, elab, mctx, lctx, eqns, true);
 }
 
 void initialize_compiler() {
diff --git a/src/library/equations_compiler/compiler.h b/src/library/equations_compiler/compiler.h
index e87094fea6..456e370015 100644
--- a/src/library/equations_compiler/compiler.h
+++ b/src/library/equations_compiler/compiler.h
@@ -9,8 +9,7 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/equations.h"
 namespace lean {
 class elaborator;
-expr compile_equations(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
-                       expr const & eqns, elaborator & elab);
+expr compile_equations(environment & env, elaborator & elab, metavar_context & mctx, local_context const & lctx, expr const & eqns);
 void initialize_compiler();
 void finalize_compiler();
 }
diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index 9f5ce63654..bf92832ecf 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -66,9 +66,8 @@ static unsigned get_eqn_compiler_max_steps(options const & o) {
 
 struct elim_match_fn {
     environment     m_env;
-    options         m_opts;
-    metavar_context m_mctx;
     elaborator &    m_elab;
+    metavar_context m_mctx;
 
     expr            m_ref;
     unsigned        m_depth{0};
@@ -86,11 +85,11 @@ struct elim_match_fn {
        an enumeration type or not. */
     name_map<bool>  m_enum;
 
-    elim_match_fn(environment const & env, options const & opts,
-                  metavar_context const & mctx, elaborator & elab):
-        m_env(env), m_opts(opts), m_mctx(mctx), m_elab(elab) {
-        m_use_ite   = get_eqn_compiler_ite(opts);
-        m_max_steps = get_eqn_compiler_max_steps(opts);
+    elim_match_fn(environment const & env, elaborator & elab,
+                  metavar_context const & mctx):
+        m_env(env), m_elab(elab), m_mctx(mctx) {
+        m_use_ite   = get_eqn_compiler_ite(elab.get_options());
+        m_max_steps = get_eqn_compiler_max_steps(elab.get_options());
     }
 
     struct equation {
@@ -193,7 +192,7 @@ struct elim_match_fn {
     }
 
     type_context mk_type_context(local_context const & lctx) {
-        return mk_type_context_for(m_env, m_opts, m_mctx, lctx);
+        return type_context(m_env, m_mctx, lctx, m_elab.get_cache(), transparency_mode::Semireducible);
     }
 
     type_context mk_type_context(expr const & mvar) {
@@ -204,9 +203,12 @@ struct elim_match_fn {
         return mk_type_context(get_local_context(P));
     }
 
+    options const & get_options() const { return m_elab.get_options(); }
+
     std::function<format(expr const &)> mk_pp_ctx(local_context const & lctx) {
-        options opts = m_opts.update(get_pp_beta_name(), false);
-        type_context ctx = mk_type_context_for(m_env, opts, m_mctx, lctx);
+        options opts = get_options();
+        opts = opts.update(get_pp_beta_name(), false);
+        type_context ctx = mk_type_context(lctx);
         return ::lean::mk_pp_ctx(ctx);
     }
 
@@ -215,7 +217,7 @@ struct elim_match_fn {
     }
 
     format nest(format const & fmt) const {
-        return ::lean::nest(get_pp_indent(m_opts), fmt);
+        return ::lean::nest(get_pp_indent(get_options()), fmt);
     }
 
     format pp_equation(equation const & eqn) {
@@ -457,7 +459,7 @@ struct elim_match_fn {
         unsigned arity = get_eqns_arity(lctx, e);
         buffer<name> var_names;
         bool use_unused_names = false;
-        optional<expr> goal = intron(m_env, m_opts, m_mctx, mvar,
+        optional<expr> goal = intron(m_env, get_options(), m_mctx, mvar,
                                      arity, var_names, use_unused_names);
         if (!goal) throw_ill_formed_eqns();
         P.m_goal       = *goal;
@@ -771,7 +773,7 @@ struct elim_match_fn {
             bool unfold_ginductive = true;
             list<name> ids;
             std::tie(new_goals, new_goal_cnames) =
-                cases(m_env, m_opts, transparency_mode::Semireducible, m_mctx,
+                cases(m_env, get_options(), transparency_mode::Semireducible, m_mctx,
                       P.m_goal, x, ids, &ilist, &slist, unfold_ginductive);
             lean_assert(length(new_goals) == length(new_goal_cnames));
             lean_assert(length(new_goals) == length(ilist));
@@ -1133,7 +1135,7 @@ struct elim_match_fn {
         buffer<expr> to_revert;
         to_revert.push_back(x);
         bool preserve_to_revert_order = true; /* it is a don't care since to_revert has size 1 */
-        expr M_1           = revert(m_env, m_opts, m_mctx, P.m_goal, to_revert, preserve_to_revert_order);
+        expr M_1           = revert(m_env, get_options(), m_mctx, P.m_goal, to_revert, preserve_to_revert_order);
 
         /* Step 2 */
         type_context ctx1  = mk_type_context(M_1);
@@ -1172,7 +1174,7 @@ struct elim_match_fn {
         /* Step 3 */
         buffer<name> new_H_names;
         bool use_unused_names = false;
-        optional<expr> M_3 = intron(m_env, m_opts, m_mctx, M_2, to_revert.size(), new_H_names, use_unused_names);
+        optional<expr> M_3 = intron(m_env, get_options(), m_mctx, M_2, to_revert.size(), new_H_names, use_unused_names);
         if (!M_3) {
             throw_error("equation compiler failed, when reintroducing reverted variables "
                         "(use 'set_option trace.eqn_compiler.elim_match true' "
@@ -1411,9 +1413,9 @@ struct elim_match_fn {
     }
 };
 
-elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx,
-                             local_context const & lctx, expr const & eqns, elaborator & elab) {
-    elim_match_fn elim(env, opts, mctx, elab);
+elim_match_result elim_match(environment & env, elaborator & elab, metavar_context & mctx,
+                             local_context const & lctx, expr const & eqns) {
+    elim_match_fn elim(env, elab, mctx);
     auto r = elim(lctx, eqns);
     env = elim.m_env;
     return r;
@@ -1426,17 +1428,17 @@ static expr get_fn_type_from_eqns(expr const & eqns) {
     return binding_domain(eqn_buffer[0]);
 }
 
-eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
-               local_context const & lctx, expr const & eqns, elaborator & elab) {
+eqn_compiler_result mk_nonrec(environment & env, elaborator & elab, metavar_context & mctx,
+                              local_context const & lctx, expr const & eqns) {
     equations_header header = get_equations_header(eqns);
-    auto R = elim_match(env, opts, mctx, lctx, eqns, elab);
+    auto R = elim_match(env, elab, mctx, lctx, eqns);
     if (header.m_is_meta || header.m_is_lemma) {
         /* Do not generate auxiliary equation or equational lemmas */
         auto fn = mk_constant(head(header.m_fn_names));
         auto counter_examples = map2<expr>(R.m_counter_examples, [&] (list<expr> const & e) { return mk_app(fn, e); });
         return { {R.m_fn}, counter_examples };
     }
-    type_context ctx1(env, opts, mctx, lctx, transparency_mode::Semireducible);
+    type_context ctx1(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
     /*
        We should use the type specified at eqns instead of m_ctx.infer(R.m_fn).
        These two types must be definitionally equal, but the shape of
@@ -1450,10 +1452,10 @@ eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_c
     name fn_name        = head(header.m_fn_names);
     name fn_actual_name = head(header.m_fn_actual_names);
     expr fn;
-    std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header,
+    std::tie(env, fn) = mk_aux_definition(env, elab.get_options(), mctx, lctx, header,
                                           fn_name, fn_actual_name, fn_type, R.m_fn);
     unsigned eqn_idx     = 1;
-    type_context ctx2(env, opts, mctx, lctx, transparency_mode::Semireducible);
+    type_context ctx2(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
     for (expr type : R.m_lemmas) {
         type_context::tmp_locals locals(ctx2);
         type = ctx2.relaxed_whnf(type);
@@ -1467,7 +1469,7 @@ eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_c
         buffer<expr> lhs_args;
         get_app_args(lhs, lhs_args);
         expr new_lhs = mk_app(fn, lhs_args);
-        env = mk_equation_lemma(env, opts, mctx, ctx2.lctx(), fn_name, fn_actual_name,
+        env = mk_equation_lemma(env, elab.get_options(), mctx, ctx2.lctx(), fn_name, fn_actual_name,
                                 eqn_idx, header.m_is_private, locals.as_buffer(), new_lhs, rhs);
         eqn_idx++;
     }
diff --git a/src/library/equations_compiler/elim_match.h b/src/library/equations_compiler/elim_match.h
index 625e51e6c5..6557388959 100644
--- a/src/library/equations_compiler/elim_match.h
+++ b/src/library/equations_compiler/elim_match.h
@@ -14,11 +14,10 @@ struct elim_match_result {
     list<expr> m_lemmas;
     list<list<expr>> m_counter_examples;
 };
-elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx,
-                local_context const & lctx, expr const & eqns, elaborator & elab);
-eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
-               local_context const & lctx, expr const & eqns,
-               elaborator & elab);
+elim_match_result elim_match(environment & env, elaborator & elab, metavar_context & mctx,
+                             local_context const & lctx, expr const & eqns);
+eqn_compiler_result mk_nonrec(environment & env, elaborator & elab, metavar_context & mctx,
+                              local_context const & lctx, expr const & eqns);
 void initialize_elim_match();
 void finalize_elim_match();
 }
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index d116140871..d0164ee779 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/util.h"
 #include "library/equations_compiler/structural_rec.h"
 #include "library/equations_compiler/elim_match.h"
+#include "frontends/lean/elaborator.h"
 
 namespace lean {
 #define trace_struct(Code) lean_trace(name({"eqn_compiler", "structural_rec"}), type_context ctx = mk_type_context(); scope_trace_env _scope1(m_env, ctx); Code)
@@ -28,7 +29,7 @@ namespace lean {
 
 struct structural_rec_fn {
     environment      m_env;
-    options          m_opts;
+    elaborator &     m_elab;
     metavar_context  m_mctx;
     local_context    m_lctx;
 
@@ -42,9 +43,9 @@ struct structural_rec_fn {
     buffer<unsigned> m_indices_pos;
     expr             m_motive_type;
 
-    structural_rec_fn(environment const & env, options const & opts,
+    structural_rec_fn(environment const & env, elaborator & elab,
                       metavar_context const & mctx, local_context const & lctx):
-        m_env(env), m_opts(opts), m_mctx(mctx), m_lctx(lctx) {
+        m_env(env), m_elab(elab), m_mctx(mctx), m_lctx(lctx) {
     }
 
     [[ noreturn ]] void throw_error(char const * msg) {
@@ -56,7 +57,7 @@ struct structural_rec_fn {
     }
 
     type_context mk_type_context() {
-        return type_context(m_env, m_opts, m_mctx, m_lctx, transparency_mode::Semireducible);
+        return type_context(m_env, m_mctx, m_lctx, m_elab.get_cache(), transparency_mode::Semireducible);
     }
 
     environment const & env() const { return m_env; }
@@ -707,7 +708,7 @@ struct structural_rec_fn {
             return new_fn;
         } else {
             expr r;
-            std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, m_header,
+            std::tie(m_env, r) = mk_aux_definition(m_env, m_elab.get_options(), m_mctx, m_lctx, m_header,
                                                    head(m_header.m_fn_names),
                                                    head(m_header.m_fn_actual_names),
                                                    m_fn_type, new_fn);
@@ -954,18 +955,18 @@ struct structural_rec_fn {
             }
             name const & fn_name        = head(m_header.m_fn_names);
             name const & fn_actual_name = head(m_header.m_fn_actual_names);
-            m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name, fn_actual_name,
+            m_env = mk_equation_lemma(m_env, m_elab.get_options(), m_mctx, ctx.lctx(), fn_name, fn_actual_name,
                                       eqn_idx, m_header.m_is_private, new_locals, new_lhs, new_rhs);
             eqn_idx++;
         }
     }
 
-    optional<eqn_compiler_result> operator()(expr const & eqns, elaborator & elab) {
+    optional<eqn_compiler_result> operator()(expr const & eqns) {
         m_ref    = eqns;
         m_header = get_equations_header(eqns);
         auto new_eqns = elim_recursion(eqns);
         if (!new_eqns) return {};
-        elim_match_result R = elim_match(m_env, m_opts, m_mctx, m_lctx, *new_eqns, elab);
+        elim_match_result R = elim_match(m_env, m_elab, m_mctx, m_lctx, *new_eqns);
         expr fn = mk_function(R.m_fn);
         if (m_header.m_aux_lemmas) {
             lean_assert(!m_header.m_is_meta);
@@ -979,10 +980,10 @@ struct structural_rec_fn {
     }
 };
 
-optional<eqn_compiler_result> try_structural_rec(environment & env, options const & opts, metavar_context & mctx,
-                                  local_context const & lctx, expr const & eqns, elaborator & elab) {
-    structural_rec_fn F(env, opts, mctx, lctx);
-    if (auto r = F(eqns, elab)) {
+optional<eqn_compiler_result> try_structural_rec(environment & env, elaborator & elab, metavar_context & mctx,
+                                                 local_context const & lctx, expr const & eqns) {
+    structural_rec_fn F(env, elab, mctx, lctx);
+    if (auto r = F(eqns)) {
         env  = F.env();
         mctx = F.mctx();
         return r;
diff --git a/src/library/equations_compiler/structural_rec.h b/src/library/equations_compiler/structural_rec.h
index a0cb530848..20f5ee9b85 100644
--- a/src/library/equations_compiler/structural_rec.h
+++ b/src/library/equations_compiler/structural_rec.h
@@ -16,9 +16,9 @@ class elaborator;
     1- \c eqns is defining more than one function
     2- None of the arguments is a primitive inductive datatype with support for brec_on
        construction, where every recursive call is structurally smaller. */
-optional<eqn_compiler_result> try_structural_rec(environment & env, options const & opts,
-                                  metavar_context & mctx, local_context const & lctx,
-                                  expr const & eqns, elaborator & elab);
+optional<eqn_compiler_result> try_structural_rec(environment & env, elaborator & elab,
+                                                 metavar_context & mctx, local_context const & lctx,
+                                                 expr const & eqns);
 
 void initialize_structural_rec();
 void finalize_structural_rec();
diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp
index 17782103f8..e1167048d4 100644
--- a/src/library/equations_compiler/unbounded_rec.cpp
+++ b/src/library/equations_compiler/unbounded_rec.cpp
@@ -19,6 +19,8 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/util.h"
 #include "library/equations_compiler/elim_match.h"
 #include "library/equations_compiler/unbounded_rec.h"
+#include "frontends/lean/elaborator.h"
+
 namespace lean {
 static expr replace_rec_apps(type_context & ctx, expr const & e) {
     equations_header const & header = get_equations_header(e);
@@ -82,10 +84,10 @@ static expr fix_rec_apps(expr const & e, name_map<expr> const & name2new_type,
         });
 }
 
-eqn_compiler_result unbounded_rec(environment & env, options const & opts,
-                   metavar_context & mctx, local_context const & lctx,
-                   expr const & e, elaborator & elab) {
-    type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
+eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
+                                  metavar_context & mctx, local_context const & lctx,
+                                  expr const & e) {
+    type_context ctx(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
 
     /* Replace recursive application with macro, and split mutual definition in n definitions. */
     expr e1 = replace_rec_apps(ctx, e);
@@ -103,7 +105,7 @@ eqn_compiler_result unbounded_rec(environment & env, options const & opts,
 
         for (unsigned fidx = 0; fidx < es.size(); fidx++) {
             unpack_eqns ues(ctx, es[fidx]);
-            auto R = elim_match(env, opts, mctx, lctx, es[fidx], elab);
+            auto R = elim_match(env, elab, mctx, lctx, es[fidx]);
             fns.push_back(helper.collect(R.m_fn));
             fn_types.push_back(helper.collect(ctx.infer(ues.get_fn(0))));
             for (list<expr> const & ts : R.m_counter_examples) {
@@ -124,8 +126,7 @@ eqn_compiler_result unbounded_rec(environment & env, options const & opts,
         equations_header const & header = get_equations_header(e);
         list<name> fn_names             = header.m_fn_names;
         list<name> fn_actual_names      = header.m_fn_actual_names;
-
-        bool zeta           = get_eqn_compiler_zeta(opts);
+        bool zeta                       = get_eqn_compiler_zeta(elab.get_options());
 
         /* 2. Update fn_types.
            zeta-expand (if needed) and apply closures. */
@@ -215,7 +216,7 @@ eqn_compiler_result unbounded_rec(environment & env, options const & opts,
 
         for (unsigned fidx = 0; fidx < es.size(); fidx++) {
             unpack_eqns ues(ctx, es[fidx]);
-            auto R = elim_match(env, opts, mctx, lctx, es[fidx], elab);
+            auto R = elim_match(env, elab, mctx, lctx, es[fidx]);
             fns.push_back(R.m_fn);
             for (list<expr> const & ts : R.m_counter_examples) {
                 counter_examples.push_back(mk_app(ues.get_fn(0), ts));
diff --git a/src/library/equations_compiler/unbounded_rec.h b/src/library/equations_compiler/unbounded_rec.h
index 1589617265..ec7ad58016 100644
--- a/src/library/equations_compiler/unbounded_rec.h
+++ b/src/library/equations_compiler/unbounded_rec.h
@@ -13,7 +13,7 @@ class elaborator;
 
     This compilation step can only be used to compile meta definitions.
     If we use it on regular definitions, the kernel will reject it. */
-eqn_compiler_result unbounded_rec(environment & env, options const & opts,
-                   metavar_context & mctx, local_context const & lctx,
-                   expr const & eqns, elaborator & elab);
+eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
+                                  metavar_context & mctx, local_context const & lctx,
+                                  expr const & eqns);
 }
diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp
index 96f5702159..766687f968 100644
--- a/src/library/equations_compiler/wf_rec.cpp
+++ b/src/library/equations_compiler/wf_rec.cpp
@@ -31,10 +31,9 @@ namespace lean {
 
 struct wf_rec_fn {
     environment      m_env;
-    options          m_opts;
+    elaborator &     m_elab;
     metavar_context  m_mctx;
     local_context    m_lctx;
-    elaborator &     m_elab;
 
     expr             m_ref;
     equations_header m_header;
@@ -44,20 +43,23 @@ struct wf_rec_fn {
 
     expr             m_dec_tac;
 
-    wf_rec_fn(environment const & env, options const & opts,
-              metavar_context const & mctx, local_context const & lctx,
-              elaborator & elab):
-        m_env(env), m_opts(opts), m_mctx(mctx), m_lctx(lctx), m_elab(elab) {
+    wf_rec_fn(environment const & env, elaborator & elab,
+              metavar_context const & mctx, local_context const & lctx):
+        m_env(env), m_elab(elab), m_mctx(mctx), m_lctx(lctx) {
     }
 
     type_context mk_type_context(local_context const & lctx) {
-        return type_context(m_env, m_opts, m_mctx, lctx, transparency_mode::Semireducible);
+        return type_context(m_env, m_mctx, lctx, m_elab.get_cache(), transparency_mode::Semireducible);
     }
 
     type_context mk_type_context() {
         return mk_type_context(m_lctx);
     }
 
+    options const & get_options() const {
+        return m_elab.get_options();
+    }
+
     expr pack_domain(expr const & eqns) {
         type_context ctx = mk_type_context();
         expr r = ::lean::pack_domain(ctx, eqns);
@@ -89,8 +91,8 @@ struct wf_rec_fn {
             lean_assert(is_pi(fn_type));
             expr d                = binding_domain(fn_type);
             expr has_well_founded = mk_app(ctx, get_has_well_founded_name(), d);
-            tactic_state s        = mk_tactic_state_for(m_env, m_opts, name(fn_name, "_wf_rec_mk_rel_tactic"), m_mctx, m_lctx, has_well_founded);
-            vm_obj r = tactic_evaluator(ctx, m_opts, m_ref)(rel_tac, extra_args, s);
+            tactic_state s        = mk_tactic_state_for(m_env, get_options(), name(fn_name, "_wf_rec_mk_rel_tactic"), m_mctx, m_lctx, has_well_founded);
+            vm_obj r = tactic_evaluator(ctx, get_options(), m_ref)(rel_tac, extra_args, s);
             if (auto new_s = tactic::is_success(r)) {
                 metavar_context mctx = new_s->mctx();
                 bool postpone_push_delayed = true;
@@ -155,10 +157,10 @@ struct wf_rec_fn {
             expr y_R_x = mk_app(m_parent.m_R, y, m_x);
 
             metavar_context mctx = m_ctx.mctx();
-            tactic_state s = mk_tactic_state_for(m_parent.m_env, m_parent.m_opts,
+            tactic_state s = mk_tactic_state_for(m_parent.m_env, m_parent.get_options(),
                                                  name(m_fn_name, "_wf_rec_mk_dec_tactic"), mctx, m_ctx.lctx(), y_R_x);
             try {
-                vm_obj r = tactic_evaluator(m_ctx, m_parent.m_opts, ref)(m_parent.m_dec_tac, s);
+                vm_obj r = tactic_evaluator(m_ctx, m_parent.get_options(), ref)(m_parent.m_dec_tac, s);
                 if (auto new_s = tactic::is_success(r)) {
                     mctx = new_s->mctx();
                     bool postpone_push_delayed = true;
@@ -276,7 +278,7 @@ struct wf_rec_fn {
         fn = mk_fix(fn);
         expr fn_type = ctx.infer(fn);
         expr r;
-        std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header,
+        std::tie(m_env, r) = mk_aux_definition(m_env, get_options(), m_mctx, m_lctx, header,
                                                head(header.m_fn_names), head(header.m_fn_actual_names),
                                                fn_type, fn);
         return r;
@@ -332,7 +334,7 @@ struct wf_rec_fn {
             expr new_lhs = mk_app(fn, app_arg(lhs));
             expr new_rhs = mk_lemma_rhs(ctx, fn, rhs);
             trace_debug_wf_aux(tout() << "aux equation [" << eqn_idx << "]:\n" << new_lhs << "\n=\n" << new_rhs << "\n";);
-            m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name, fn_prv_name,
+            m_env = mk_equation_lemma(m_env, get_options(), m_mctx, ctx.lctx(), fn_name, fn_prv_name,
                                       eqn_idx, m_header.m_is_private, locals.as_buffer(), new_lhs, new_rhs);
             eqn_idx++;
         }
@@ -456,7 +458,7 @@ struct wf_rec_fn {
             fn_actual_names     = tail(fn_actual_names);
             trace_debug_wf(tout() << fn_name << " := " << fn_val << "\n";);
             expr r;
-            std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header, fn_name, fn_actual_name,
+            std::tie(m_env, r) = mk_aux_definition(m_env, get_options(), m_mctx, m_lctx, header, fn_name, fn_actual_name,
                                                    fn_type, fn_val);
             result_fns.push_back(r);
         }
@@ -556,7 +558,7 @@ struct wf_rec_fn {
         trace_debug_wf(tout() << "after elim_recursion\n" << eqns << "\n";);
 
         /* Eliminate pattern matching */
-        elim_match_result r = elim_match(m_env, m_opts, m_mctx, m_lctx, eqns, m_elab);
+        elim_match_result r = elim_match(m_env, m_elab, m_mctx, m_lctx, eqns);
         expr fn = mk_fix_aux_function(get_equations_header(eqns), r.m_fn);
 
         trace_debug_wf(tout() << "after mk_fix\n" << fn << " :\n  " << mk_type_context().infer(fn) << "\n";);
@@ -573,10 +575,10 @@ struct wf_rec_fn {
 
 /** \brief (Try to) eliminate "recursive calls" in the equations \c eqns by using well founded recursion.
     If successful, elim_match is used to compile pattern matching. */
-eqn_compiler_result wf_rec(environment & env, options const & opts,
-            metavar_context & mctx, local_context const & lctx,
-            expr const & eqns, elaborator & elab) {
-    wf_rec_fn proc(env, opts, mctx, lctx, elab);
+eqn_compiler_result wf_rec(environment & env, elaborator & elab,
+                           metavar_context & mctx, local_context const & lctx,
+                           expr const & eqns) {
+    wf_rec_fn proc(env, elab, mctx, lctx);
     auto r = proc(eqns);
     env    = proc.m_env;
     mctx   = proc.m_mctx;
diff --git a/src/library/equations_compiler/wf_rec.h b/src/library/equations_compiler/wf_rec.h
index dc1921ac64..2432ef7457 100644
--- a/src/library/equations_compiler/wf_rec.h
+++ b/src/library/equations_compiler/wf_rec.h
@@ -9,9 +9,9 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/util.h"
 namespace lean {
 class elaborator;
-eqn_compiler_result wf_rec(environment & env, options const & opts,
-            metavar_context & mctx, local_context const & lctx,
-            expr const & eqns, elaborator & elab);
+eqn_compiler_result wf_rec(environment & env, elaborator & elab,
+                           metavar_context & mctx, local_context const & lctx,
+                           expr const & eqns);
 
 /* Return true if definition `n` was compiled by equation compiler using
    well_founded recursion. */
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 049648ea6a..886118c3b3 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -560,6 +560,8 @@ public:
         type_context(env, options(), metavar_context(), local_context(), m) {}
     type_context(environment const & env, options const & o, transparency_mode m = transparency_mode::Reducible):
         type_context(env, o, metavar_context(), local_context(), m) {}
+    type_context(environment const & env, abstract_context_cache & cache, transparency_mode m = transparency_mode::Reducible):
+        type_context(env, metavar_context(), local_context(), cache, m) {}
     type_context(type_context const &) = delete;
     type_context(type_context &&) = default;
     virtual ~type_context();