diff --git a/stage0/src/library/CMakeLists.txt b/stage0/src/library/CMakeLists.txt
index bf27a112d7..7e12c55b6f 100644
--- a/stage0/src/library/CMakeLists.txt
+++ b/stage0/src/library/CMakeLists.txt
@@ -4,8 +4,7 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp
   class.cpp util.cpp print.cpp annotation.cpp
   protected.cpp reducible.cpp init_module.cpp exception.cpp
   pp_options.cpp projection.cpp
-  idx_metavar.cpp aux_recursors.cpp trace.cpp
-  local_context.cpp metavar_context.cpp
+  aux_recursors.cpp trace.cpp
   type_context.cpp
   locals.cpp messages.cpp message_builder.cpp check.cpp
   profiling.cpp time_task.cpp
diff --git a/stage0/src/library/abstract_type_context.h b/stage0/src/library/abstract_type_context.h
index 99a8e1bb7c..eb6ded4cc4 100644
--- a/stage0/src/library/abstract_type_context.h
+++ b/stage0/src/library/abstract_type_context.h
@@ -6,16 +6,12 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr.h"
-#include "library/local_context.h"
-#include "library/metavar_context.h"
 
 namespace lean {
 class abstract_type_context {
 public:
     virtual ~abstract_type_context() {}
     virtual environment const & env() const = 0;
-    virtual local_context const & lctx() const = 0;
-    virtual metavar_context const & mctx() const = 0;
     virtual expr whnf(expr const & e) = 0;
     virtual name next_name() = 0;
     virtual expr relaxed_whnf(expr const & e) { return whnf(e); }
diff --git a/stage0/src/library/cache_helper.h b/stage0/src/library/cache_helper.h
deleted file mode 100644
index 85c1b72dd4..0000000000
--- a/stage0/src/library/cache_helper.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <memory>
-#include "library/type_context.h"
-
-namespace lean {
-/** \brief Helper class for making sure we have a cache that is compatible
-    with a given environment and transparency mode. */
-template<typename Cache>
-class cache_compatibility_helper {
-    std::unique_ptr<Cache> m_cache_ptr[LEAN_NUM_TRANSPARENCY_MODES];
-public:
-    Cache & get_cache_for(environment const & env, transparency_mode m) {
-        unsigned midx = static_cast<unsigned>(m);
-        if (!m_cache_ptr[midx] || !is_eqp(env, m_cache_ptr[midx]->env())) {
-            m_cache_ptr[midx].reset(new Cache(env));
-        }
-        return *m_cache_ptr[midx].get();
-    }
-
-    Cache & get_cache_for(type_context_old const & ctx) {
-        return get_cache_for(ctx.env(), ctx.mode());
-    }
-
-    void clear() {
-        for (unsigned i = 0; i < LEAN_NUM_TRANSPARENCY_MODES; i++) m_cache_ptr[i].reset();
-    }
-};
-}
diff --git a/stage0/src/library/check.cpp b/stage0/src/library/check.cpp
index 8e11f8caf3..8b35b9b184 100644
--- a/stage0/src/library/check.cpp
+++ b/stage0/src/library/check.cpp
@@ -13,131 +13,12 @@ namespace lean {
 struct check_fn {
     type_context_old &   m_ctx;
     expr_set             m_visited;
-
-    void visit_constant(expr const & e) {
-        constant_info info = m_ctx.env().get(const_name(e));
-        if (info.get_num_lparams() != length(const_levels(e))) {
-            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
-                       tout() << "incorrect of universe levels at " << e << "\n";);
-            throw exception("check failed, incorrect number of universe levels "
-                            "(use 'set_option trace.check true' for additional details)");
-        }
-    }
-
-    void ensure_type(expr const & e) {
-        expr S = m_ctx.relaxed_whnf(m_ctx.infer(e));
-        if (is_sort(S)) return;
-        if (is_metavar(S)) {
-            level u = m_ctx.mk_univ_metavar_decl();
-            if (m_ctx.is_def_eq(S, mk_sort(u)))
-                return;
-        }
-        lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
-                   tout() << "type expected at " << e << "\n";);
-        throw exception("check failed, type expected "
-                        "(use 'set_option trace.check true' for additional details)");
-    }
-
-    void visit_binding(expr const & e, bool is_pi) {
-        type_context_old::tmp_locals locals(m_ctx);
-        expr it = e;
-        while (it.kind() == e.kind()) {
-            expr d = instantiate_rev(binding_domain(it), locals.size(), locals.data());
-            visit(d);
-            locals.push_local(binding_name(it), d, binding_info(it));
-            ensure_type(d);
-            it = binding_body(it);
-        }
-        expr b = instantiate_rev(it, locals.size(), locals.data());
-        visit(b);
-        if (is_pi)
-            ensure_type(b);
-    }
-
-    void visit_lambda(expr const & e) {
-        visit_binding(e, false);
-    }
-
-    void visit_pi(expr const & e) {
-        visit_binding(e, true);
-    }
-
-    void visit_let(expr const & e) {
-        visit(let_value(e));
-        visit(let_type(e));
-        expr v_type = m_ctx.infer(let_value(e));
-        if (!m_ctx.relaxed_is_def_eq(let_type(e), v_type)) {
-            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
-                       tout() << "type mismatch at let binder\n  " << e << "\n";);
-            throw exception("check failed, type mismatch at let binder "
-                            "(use 'set_option trace.check true' for additional details)");
-        }
-        /* Improve performance if bottleneck */
-        type_context_old::tmp_locals locals(m_ctx);
-        expr local = locals.push_local_from_let(e);
-        visit(instantiate(let_body(e), local));
-    }
-
-    void visit_app(expr const & e) {
-        visit(app_fn(e));
-        visit(app_arg(e));
-        expr f_type = m_ctx.relaxed_whnf(m_ctx.infer(app_fn(e)));
-        if (!is_pi(f_type)) {
-            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
-                       tout() << "function expected at\n  " << e << "\ntype\n  " << f_type << "\n";);
-            throw exception("check failed, function expected (use 'set_option trace.check true' for additional details)");
-        }
-        expr a_type = m_ctx.infer(app_arg(e));
-        expr d_type = binding_domain(f_type);
-        if (!m_ctx.relaxed_is_def_eq(a_type, d_type)) {
-            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
-                       tout() << "application type mismatch at\n  " << e << "\nargument type\n  "
-                       << a_type << "\nexpected type\n  " << d_type;);
-            throw exception("check failed, application type mismatch "
-                            "(use 'set_option trace.check true' for additional details)");
-        }
-    }
-
-    void visit(expr const & e) {
-        if (m_visited.find(e) != m_visited.end())
-            return;
-        m_visited.insert(e);
-        switch (e.kind()) {
-        case expr_kind::FVar:
-        case expr_kind::MVar:
-        case expr_kind::Sort:
-        case expr_kind::Lit:
-        case expr_kind::Local:
-            break; /* do nothing */
-        case expr_kind::Const:
-            return visit_constant(e);
-        case expr_kind::BVar:
-            lean_unreachable();  // LCOV_EXCL_LINE
-        case expr_kind::Lambda:
-            return visit_lambda(e);
-        case expr_kind::Pi:
-            return visit_pi(e);
-        case expr_kind::App:
-            return visit_app(e);
-        case expr_kind::Let:
-            return visit_let(e);
-        case expr_kind::MData:
-            return visit(mdata_expr(e));
-        case expr_kind::Proj:
-            return visit(proj_expr(e));
-        }
-    }
-
 public:
     check_fn(type_context_old & ctx):m_ctx(ctx) {}
-    void operator()(expr const & e) { return visit(e); }
 };
 
-void check(type_context_old & ctx, expr const & e) {
-    metavar_context mctx = ctx.mctx();
-    check_fn checker(ctx);
-    checker(e);
-    ctx.set_mctx(mctx);
+void check(type_context_old &, expr const &) {
+    lean_unreachable();
 }
 
 void initialize_check() {
diff --git a/stage0/src/library/compiler/util.cpp b/stage0/src/library/compiler/util.cpp
index 25449fc697..541dafb07e 100644
--- a/stage0/src/library/compiler/util.cpp
+++ b/stage0/src/library/compiler/util.cpp
@@ -416,7 +416,7 @@ bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & t
 
 bool is_irrelevant_type(environment const & env, expr const & type) {
     type_checker::state st(env);
-    return is_irrelevant_type(st, local_context(), type);
+    return is_irrelevant_type(st, local_ctx(), type);
 }
 
 void collect_used(expr const & e, name_hash_set & S) {
diff --git a/stage0/src/library/expr_lt.cpp b/stage0/src/library/expr_lt.cpp
index 3c99929867..8c4bea62b8 100644
--- a/stage0/src/library/expr_lt.cpp
+++ b/stage0/src/library/expr_lt.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "library/expr_lt.h"
 
 namespace lean {
-bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const * lctx) {
+bool is_lt(expr const & a, expr const & b, bool use_hash, local_ctx const * lctx) {
     if (is_eqp(a, b))                    return false;
     if (a.kind() != b.kind())            return a.kind() < b.kind();
     if (use_hash) {
diff --git a/stage0/src/library/expr_lt.h b/stage0/src/library/expr_lt.h
index 66ee23eef6..490c4fef14 100644
--- a/stage0/src/library/expr_lt.h
+++ b/stage0/src/library/expr_lt.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "util/rb_map.h"
-#include "library/local_context.h"
+#include "kernel/local_ctx.h"
 
 namespace lean {
 /** \brief Total order on expressions.
@@ -18,7 +18,7 @@ namespace lean {
 
     \remark If lctx is not nullptr, then we use the local_decl index to compare local constants.
 */
-bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const * lctx = nullptr);
+bool is_lt(expr const & a, expr const & b, bool use_hash, local_ctx const * lctx = nullptr);
 /** \brief Similar to is_lt, but universe level parameter names are ignored. */
 bool is_lt_no_level_params(expr const & a, expr const & b);
 inline bool is_hash_lt(expr const & a, expr const & b) { return is_lt(a, b, true); }
diff --git a/stage0/src/library/idx_metavar.cpp b/stage0/src/library/idx_metavar.cpp
deleted file mode 100644
index 1140cde4b9..0000000000
--- a/stage0/src/library/idx_metavar.cpp
+++ /dev/null
@@ -1,104 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <lean/interrupt.h>
-#include "kernel/for_each_fn.h"
-#include "library/idx_metavar.h"
-#include "library/metavar_context.h"
-#include "library/replace_visitor.h"
-
-#ifndef LEAN_INSTANTIATE_METAIDX_CACHE_CAPACITY
-#define LEAN_INSTANTIATE_METAIDX_CACHE_CAPACITY 1024*8
-#endif
-
-namespace lean {
-static name * g_tmp_prefix = nullptr;
-
-void initialize_idx_metavar() {
-    g_tmp_prefix = new name(name::mk_internal_unique_name());
-    mark_persistent(g_tmp_prefix->raw());
-}
-
-void finalize_idx_metavar() {
-    delete g_tmp_prefix;
-}
-
-level mk_idx_metauniv(unsigned i) {
-    return mk_univ_mvar(name(*g_tmp_prefix, i));
-}
-
-expr mk_idx_metavar(unsigned i) {
-    return mk_metavar(name(*g_tmp_prefix, i));
-}
-
-bool is_idx_metauniv(level const & l) {
-    if (!is_mvar(l))
-        return false;
-    name const & n = mvar_id(l);
-    return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix;
-}
-
-unsigned to_meta_idx(level const & l) {
-    lean_assert(is_idx_metauniv(l));
-    return mvar_id(l).get_numeral().get_small_value();
-}
-
-bool is_idx_metavar(expr const & e) {
-    if (!is_metavar(e))
-        return false;
-    name const & n = mvar_name(e);
-    return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix;
-}
-
-unsigned to_meta_idx(expr const & e) {
-    lean_assert(is_idx_metavar(e));
-    return mvar_name(e).get_numeral().get_small_value();
-}
-
-bool has_idx_metauniv(level const & l) {
-    if (!has_mvar(l))
-        return false;
-    bool found = false;
-    for_each(l, [&](level const & l) {
-            if (found) return false;
-            if (!has_mvar(l)) return false;
-            if (is_idx_metauniv(l))
-                found = true;
-            return true;
-        });
-    return found;
-}
-
-bool has_idx_metavar(expr const & e) {
-    if (!has_univ_metavar(e) && !has_expr_metavar(e))
-        return false;
-    bool found = false;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (found) return false;
-            if (!has_univ_metavar(e) && !has_expr_metavar(e)) return false;
-            if (is_idx_metavar(e))
-                found = true;
-            else if (is_constant(e) && std::any_of(const_levels(e).begin(), const_levels(e).end(), has_idx_metauniv))
-                found = true;
-            else if (is_sort(e) && has_idx_metauniv(sort_level(e)))
-                found = true;
-            return true;
-        });
-    return found;
-}
-
-bool has_idx_expr_metavar(expr const & e) {
-    if (!has_expr_metavar(e))
-        return false;
-    bool found = false;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (found || !has_expr_metavar(e)) return false;
-            if (is_idx_metavar(e)) found = true;
-            return true;
-        });
-    return found;
-}
-}
diff --git a/stage0/src/library/idx_metavar.h b/stage0/src/library/idx_metavar.h
deleted file mode 100644
index 584d8dd27b..0000000000
--- a/stage0/src/library/idx_metavar.h
+++ /dev/null
@@ -1,39 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-namespace lean {
-/** \brief Create a universe level metavariable that can be used as a placeholder in #match.
-
-    \remark The index \c i is encoded in the hierarchical name, and can be quickly accessed.
-    In the match procedure the substitution is also efficiently represented as an array (aka buffer).
-*/
-level mk_idx_metauniv(unsigned i);
-/** \brief Return true iff \c l is a metauniverse created using \c mk_idx_metauniv */
-bool is_idx_metauniv(level const & l);
-unsigned to_meta_idx(level const & l);
-
-/** \brief Create a special metavariable that can be used as a placeholder in #match.
-
-    \remark The index \c i is encoded in the hierarchical name, and can be quickly accessed.
-    In the match procedure the substitution is also efficiently represented as an array (aka buffer).
-*/
-expr mk_idx_metavar(unsigned i);
-/** \brief Return true iff \c l is a metavariable created using \c mk_idx_metavar */
-bool is_idx_metavar(expr const & l);
-unsigned to_meta_idx(expr const & e);
-
-/** \brief Return true iff \c e contains idx metavariables or universe metavariables */
-bool has_idx_metavar(expr const & e);
-bool has_idx_expr_metavar(expr const & e);
-bool has_idx_metauniv(level const & l);
-
-class metavar_context;
-
-void initialize_idx_metavar();
-void finalize_idx_metavar();
-}
diff --git a/stage0/src/library/init_module.cpp b/stage0/src/library/init_module.cpp
index 304ca15850..80a9c7ea69 100644
--- a/stage0/src/library/init_module.cpp
+++ b/stage0/src/library/init_module.cpp
@@ -11,14 +11,11 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 #include "library/protected.h"
 #include "library/io_state.h"
-#include "library/idx_metavar.h"
 #include "library/placeholder.h"
 #include "library/print.h"
 #include "library/util.h"
 #include "library/pp_options.h"
 #include "library/type_context.h"
-#include "library/local_context.h"
-#include "library/metavar_context.h"
 #include "library/check.h"
 #include "library/profiling.h"
 #include "library/time_task.h"
@@ -43,11 +40,8 @@ void finalize_library_core_module() {
 }
 
 void initialize_library_module() {
-    initialize_local_context();
-    initialize_metavar_context();
     initialize_print();
     initialize_placeholder();
-    initialize_idx_metavar();
     initialize_io_state();
     initialize_num();
     initialize_annotation();
@@ -69,10 +63,7 @@ void finalize_library_module() {
     finalize_annotation();
     finalize_num();
     finalize_io_state();
-    finalize_idx_metavar();
     finalize_placeholder();
     finalize_print();
-    finalize_metavar_context();
-    finalize_local_context();
 }
 }
diff --git a/stage0/src/library/local_context.cpp b/stage0/src/library/local_context.cpp
deleted file mode 100644
index 3a2bc8b872..0000000000
--- a/stage0/src/library/local_context.cpp
+++ /dev/null
@@ -1,437 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <algorithm>
-#include <limits>
-#include "util/fresh_name.h"
-#include "util/list_fn.h"
-#include "kernel/for_each_fn.h"
-#include "kernel/find_fn.h"
-#include "kernel/replace_fn.h"
-#include "library/pp_options.h"
-#include "library/local_context.h"
-#include "library/metavar_context.h"
-#include "library/trace.h"
-
-namespace lean {
-name mk_local_decl_name() {
-    return mk_fresh_name();
-}
-
-struct depends_on_fn {
-    metavar_context const & m_mctx;
-    local_context const *   m_lctx;
-    unsigned                m_num;
-    expr const *            m_locals;
-    name_set                m_visited_mvars;
-    name_set                m_visited_decls;
-
-    depends_on_fn(metavar_context const & mctx, local_context const & lctx, unsigned num, expr const * locals):
-        m_mctx(mctx), m_lctx(&lctx), m_num(num), m_locals(locals) {
-        lean_assert(std::all_of(locals, locals+num, is_fvar));
-    }
-
-    depends_on_fn(metavar_context const & mctx, unsigned num, expr const * locals):
-        m_mctx(mctx), m_lctx(nullptr), m_num(num), m_locals(locals) {
-        lean_assert(std::all_of(locals, locals+num, is_fvar));
-    }
-
-    bool visit_local(expr const & e) {
-        lean_assert(is_fvar(e));
-        if (std::any_of(m_locals, m_locals + m_num,
-                        [&](expr const & l) { return fvar_name(e) == fvar_name(l); }))
-            return true;
-
-        if (!m_lctx || m_visited_decls.contains(fvar_name(e)))
-            return false;
-        m_visited_decls.insert(fvar_name(e));
-        optional<local_decl> decl = m_lctx->find_local_decl(e);
-        if (!decl)
-            return false;
-        if (visit(decl->get_type()))
-            return true;
-        if (optional<expr> v = decl->get_value())
-            return visit(*v);
-        else
-            return false;
-    }
-
-    bool visit_metavar(expr const & e) {
-        lean_assert(is_metavar_decl_ref(e));
-        if (m_visited_mvars.contains(mvar_name(e)))
-            return false;
-        m_visited_mvars.insert(mvar_name(e));
-        optional<metavar_decl> decl = m_mctx.find_metavar_decl(e);
-        if (!decl)
-            return false;
-        if (visit(decl->get_type()))
-            return true;
-        if (auto v = m_mctx.get_assignment(e)) {
-            if (visit(*v))
-                return true;
-        }
-        return false;
-    }
-
-    bool visit(expr const & e) {
-        if (!has_local(e) && !has_expr_metavar(e))
-            return false;
-        bool found = false;
-        for_each(e, [&](expr const & e, unsigned) {
-                if (found) return false;
-                if (!has_local(e) && !has_expr_metavar(e)) return false;
-                if (is_fvar(e) && visit_local(e)) {
-                    found = true;
-                    return false;
-                }
-                if (is_metavar_decl_ref(e) && visit_metavar(e)) {
-                    found = true;
-                    return false;
-                }
-                return true;
-            });
-        return found;
-    }
-
-    bool operator()(expr const & e) { return visit(e); }
-};
-
-bool depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals) {
-    return depends_on_fn(mctx, num, locals)(e);
-}
-
-bool depends_on(local_decl const & d, metavar_context const & mctx, unsigned num, expr const * locals) {
-    depends_on_fn fn(mctx, num, locals);
-    if (fn(d.get_type()))
-        return true;
-    if (auto v = d.get_value()) {
-        return fn(*v);
-    }
-    return false;
-}
-
-bool depends_on(expr const & e, metavar_context const & mctx, buffer<expr> const & locals) {
-    return depends_on_fn(mctx, locals.size(), locals.data())(e);
-}
-
-bool depends_on(local_decl const & d, metavar_context const & mctx, buffer<expr> const & locals) {
-    return depends_on(d, mctx, locals.size(), locals.data());
-}
-
-bool depends_on(expr const & e, metavar_context const & mctx, local_context const & lctx, unsigned num, expr const * locals) {
-    return depends_on_fn(mctx, lctx, num, locals)(e);
-}
-
-local_decl local_context::mk_local_decl_core(name const & n, name const & un, expr const & type, binder_info bi) {
-    return local_ctx::mk_local_decl(n, un, type, bi);
-}
-
-local_decl local_context::mk_local_decl_core(name const & n, name const & un, expr const & type, expr const & value) {
-    return local_ctx::mk_local_decl(n, un, type, value);
-}
-
-expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, optional<expr> const & value, binder_info bi) {
-    local_decl d = value ? local_ctx::mk_local_decl(n, un, type, *value) : local_ctx::mk_local_decl(n, un, type, bi);
-    expr r = d.mk_ref();
-    lean_assert(is_fvar(r));
-    return r;
-}
-
-expr local_context::mk_local_decl(expr const & type, binder_info bi) {
-    name n = mk_local_decl_name();
-    return mk_local_decl(n, n, type, none_expr(), bi);
-}
-
-expr local_context::mk_local_decl(expr const & type, expr const & value) {
-    name n = mk_local_decl_name();
-    return mk_local_decl(n, n, type, some_expr(value), mk_binder_info());
-}
-
-expr local_context::mk_local_decl(name const & un, expr const & type, binder_info bi) {
-    return mk_local_decl(mk_local_decl_name(), un, type, none_expr(), bi);
-}
-
-expr local_context::mk_local_decl(name const & un, expr const & type, expr const & value) {
-    return mk_local_decl(mk_local_decl_name(), un, type, some_expr(value), mk_binder_info());
-}
-
-expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi) {
-    return mk_local_decl(n, un, type, none_expr(), bi);
-}
-
-expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, expr const & value) {
-    return mk_local_decl(n, un, type, some_expr(value), mk_binder_info());
-}
-
-extern "C" object* lean_local_ctx_num_indices(object* lctx);
-extern "C" object* lean_local_ctx_get(object* lctx, object* idx);
-
-unsigned local_context::num_indices() const {
-    return unbox(lean_local_ctx_num_indices(to_obj_arg()));
-}
-
-optional<local_decl> local_context::get_decl_at(unsigned idx) const {
-    return to_optional<local_decl>(lean_local_ctx_get(to_obj_arg(), box(idx)));
-}
-
-optional<local_decl> local_context::back_find_if(std::function<bool(local_decl const &)> const & pred) const { // NOLINT
-    unsigned i = num_indices();
-    while (i > 0) {
-        --i;
-        optional<local_decl> decl = get_decl_at(i);
-        if (decl && pred(*decl)) return decl;
-    }
-    return optional<local_decl>();
-}
-
-optional<local_decl> local_context::find_local_decl_from_user_name(name const & n) const {
-    return back_find_if([&](local_decl const & d) { return d.get_user_name() == n; });
-}
-
-optional<local_decl> local_context::find_last_local_decl() const {
-    unsigned i = num_indices();
-    while (i > 0) {
-        --i;
-        optional<local_decl> decl = get_decl_at(i);
-        if (decl) return decl;
-    }
-    return optional<local_decl>();
-}
-
-local_decl local_context::get_last_local_decl() const {
-    if (auto decl = find_last_local_decl())
-        return *decl;
-    throw("unknown local constant, context is empty");
-}
-
-void local_context::for_each(std::function<void(local_decl const &)> const & fn) const {
-    unsigned num = num_indices();
-    for (unsigned i = 0; i < num; i++) {
-        optional<local_decl> decl = get_decl_at(i);
-        if (decl) fn(*decl);
-    }
-}
-
-optional<local_decl> local_context::find_if(std::function<bool(local_decl const &)> const & pred) const {
-    unsigned num = num_indices();
-    for (unsigned i = 0; i < num; i++) {
-        optional<local_decl> decl = get_decl_at(i);
-        if (decl && pred(*decl)) return decl;
-    }
-    return optional<local_decl>();
-}
-
-void local_context::for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const {
-    unsigned num = num_indices();
-    for (unsigned i = d.get_idx() + 1; i < num; i++) {
-        optional<local_decl> decl = get_decl_at(i);
-        if (decl) fn(*decl);
-    }
-}
-
-extern "C" object* lean_local_ctx_pop(object* lctx);
-
-void local_context::pop_local_decl() {
-    m_obj = lean_local_ctx_pop(m_obj);
-}
-
-optional<local_decl> local_context::has_dependencies(local_decl const & d, metavar_context const & mctx) const {
-    lean_assert(find_local_decl(d.get_name()));
-    expr l = d.mk_ref();
-    optional<local_decl> r;
-    for_each_after(d, [&](local_decl const & d2) {
-            if (r) return;
-            if (depends_on(d2, mctx, 1, &l))
-                r = d2;
-        });
-    return r;
-}
-
-bool local_context::is_subset_of(name_set const & ls) const {
-    // TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class
-    return !static_cast<bool>(find_if([&](local_decl const & d) {
-                return !ls.contains(d.get_name());
-            }));
-}
-
-bool local_context::is_subset_of(local_context const & ctx) const {
-    // TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class
-    return !static_cast<bool>(find_if([&](local_decl const & d) {
-                return !ctx.find_local_decl(d.get_name());
-            }));
-}
-
-local_context local_context::remove(buffer<expr> const & locals) const {
-    lean_assert(std::all_of(locals.begin(), locals.end(),
-                            [&](expr const & l) {
-                                return is_fvar(l) && find_local_decl(l);
-                            }));
-    /* TODO(Leo): check whether the following loop is a performance bottleneck. */
-    local_context r          = *this;
-    for (expr const & l : locals) {
-        local_decl d = get_local_decl(l);
-        r.clear(d);
-    }
-    lean_assert(r.well_formed());
-    return r;
-}
-
-/* Return true iff all local_decl references in \c e are in \c s. */
-static bool locals_subset_of(expr const & e, name_set const & s) {
-    bool ok = true;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (!ok) return false; // stop search
-            if (is_fvar(e) && !s.contains(fvar_name(e))) {
-                ok = false;
-                return false;
-            }
-            return true;
-        });
-    return ok;
-}
-
-bool local_context::well_formed() const {
-    bool ok = true;
-    name_set found_locals;
-    for_each([&](local_decl const & d) {
-            if (!locals_subset_of(d.get_type(), found_locals)) {
-                ok = false;
-                lean_unreachable();
-            }
-            if (auto v = d.get_value()) {
-                if (!locals_subset_of(*v, found_locals)) {
-                    ok = false;
-                    lean_unreachable();
-                }
-            }
-            found_locals.insert(d.get_name());
-        });
-    return ok;
-}
-
-bool local_context::well_formed(expr const & e) const {
-    bool ok = true;
-    ::lean::for_each(e, [&](expr const & e, unsigned) {
-            if (!ok) return false;
-            if (is_fvar(e) && !find_local_decl(e)) {
-                ok = false;
-            }
-            return true;
-        });
-    return ok;
-}
-
-format local_context::pp(formatter const & fmt) const { // NOLINT
-    options const & opts = fmt.get_options();
-    unsigned indent      = get_pp_indent(opts);
-    unsigned max_hs      = get_pp_goal_max_hyps(opts);
-    bool first           = true;
-    unsigned i           = 0;
-    format ids;
-    optional<expr> type;
-    format r;
-    for_each([&](local_decl const & d) {
-            if (i >= max_hs)
-                return;
-            i++;
-            if (type && (d.get_type() != *type || d.get_value())) {
-                // add (ids : type) IF the d.get_type() != type OR d is a let-decl
-                if (first) first = false;
-                else r += format(",") + line();
-
-                r += group(ids + space() + format(":") + nest(indent, line() + fmt(*type)));
-                type = optional<expr>();
-                ids  = format();
-            }
-
-            name n = sanitize_if_fresh(d.get_user_name());
-            n = sanitize_name_generator_name(n);
-
-            if (d.get_value()) {
-                if (first) first = false;
-                else r += format(",") + line();
-                r += group(format(n) + space() + format(":") + space() + fmt(d.get_type()) +
-                           space() + format(":=") + nest(indent, line() + fmt(*d.get_value())));
-            } else if (!type) {
-                lean_assert(!d.get_value());
-                ids  = format(n);
-                type = d.get_type();
-            } else {
-                lean_assert(!d.get_value());
-                lean_assert(type && d.get_type() == *type);
-                ids += space() + format(n);
-            }
-        });
-    if (type) {
-        if (!first) r += format(",") + line();
-        r += group(ids + space() + format(":") + nest(indent, line() + fmt(*type)));
-    }
-    if (get_pp_goal_compact(opts))
-        r = group(r);
-    return r;
-}
-
-bool local_context::uses_user_name(name const & n) const {
-    return static_cast<bool>(find_if([&](local_decl const & d) { return d.get_user_name() == n; }));
-}
-
-name local_context::get_unused_name(name const & prefix, unsigned & idx) const {
-    while (true) {
-        name curr = prefix.append_after(idx);
-        idx++;
-        if (!uses_user_name(curr))
-            return curr;
-    }
-}
-
-name local_context::get_unused_name(name const & suggestion) const {
-  if (!uses_user_name(suggestion))
-        return suggestion;
-    unsigned idx = 1;
-    return get_unused_name(suggestion, idx);
-}
-
-local_context local_context::instantiate_mvars(metavar_context & mctx) const {
-    local_context r;
-    for_each([&](local_decl const & d) {
-            expr new_type = mctx.instantiate_mvars(d.get_type());
-            if (auto v = d.get_value())
-                r.mk_local_decl_core(d.get_name(), d.get_user_name(), new_type, mctx.instantiate_mvars(*v));
-            else
-                r.mk_local_decl_core(d.get_name(), d.get_user_name(), new_type, d.get_info());
-        });
-    return r;
-}
-
-bool contains_let_local_decl(local_context const & lctx, expr const & e) {
-    if (!has_local(e)) return false;
-    return static_cast<bool>(find(e, [&](expr const & e, unsigned) {
-                if (!is_fvar(e)) return false;
-                optional<local_decl> d = lctx.find_local_decl(e);
-                return d && d->get_value();
-            }));
-}
-
-expr zeta_expand(local_context const & lctx, expr const & e) {
-    if (!contains_let_local_decl(lctx, e)) return e;
-    return replace(e, [&](expr const & e, unsigned) {
-            if (!has_local(e)) return some_expr(e);
-            if (is_fvar(e)) {
-                if (auto d = lctx.find_local_decl(e)) {
-                    if (auto v = d->get_value())
-                        return some_expr(zeta_expand(lctx, *v));
-                }
-            }
-            return none_expr();
-        });
-}
-
-void initialize_local_context() {
-}
-
-void finalize_local_context() {
-}
-}
diff --git a/stage0/src/library/local_context.h b/stage0/src/library/local_context.h
deleted file mode 100644
index edeb45860b..0000000000
--- a/stage0/src/library/local_context.h
+++ /dev/null
@@ -1,136 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/name_map.h"
-#include "util/name_set.h"
-#include "kernel/local_ctx.h"
-#include "kernel/expr.h"
-#include "library/formatter.h"
-
-namespace lean {
-class metavar_context;
-class local_context;
-bool depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals);
-bool depends_on(local_decl const & d, metavar_context const & mctx,  unsigned num, expr const * locals);
-bool depends_on(expr const & e, metavar_context const & mctx,  buffer<expr> const & locals);
-bool depends_on(local_decl const & d, metavar_context const & mctx, buffer<expr> const & locals);
-
-/* Similar to depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals), but it
-   will also visit the value v of local definitions (x : t := v) if x occurs in e (directly or indirectly). */
-bool depends_on(expr const & e, metavar_context const & mctx, local_context const & lctx, unsigned num, expr const * locals);
-inline bool depends_on(expr const & e, metavar_context const & mctx, local_context const & lctx, expr const & local) {
-    return depends_on(e, mctx, lctx, 1, &local);
-}
-
-/* Create an unieq local_decl name.
-   This is a low-level function. The high-level methods
-   at local_context use this function internally. */
-name mk_local_decl_name();
-
-class metavar_context;
-
-/* Extend kernel local context object with support for generating "unused" user-names and
-   "freezing" local instances. */
-class local_context : public local_ctx {
-    friend class type_context_old;
-
-    local_context remove(buffer<expr> const & locals) const;
-    expr mk_local_decl(name const & n, name const & un, expr const & type,
-                       optional<expr> const & value, binder_info bi);
-    local_decl mk_local_decl_core(name const & n, name const & un, expr const & type, binder_info bi);
-    local_decl mk_local_decl_core(name const & n, name const & un, expr const & type, expr const & value);
-    unsigned num_indices() const;
-    optional<local_decl> get_decl_at(unsigned idx) const;
-public:
-    local_context() {}
-    explicit local_context(obj_arg o):local_ctx(o) {}
-    local_context(b_obj_arg o, bool):local_ctx(o, true) {}
-
-    expr mk_local_decl(expr const & type, binder_info bi = mk_binder_info());
-    expr mk_local_decl(expr const & type, expr const & value);
-    expr mk_local_decl(name const & un, expr const & type, binder_info bi = mk_binder_info());
-    expr mk_local_decl(name const & un, expr const & type, expr const & value);
-
-    /* Low-level version of the methods above.
-
-       \pre `n` was created using mk_local_decl_name
-       \pre there is no local_decl named `n` in this local_context. */
-    expr mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi = mk_binder_info());
-    expr mk_local_decl(name const & n, name const & un, expr const & type, expr const & value);
-
-    /** \brief Return the most recently added local_decl \c d s.t. d.get_user_name() == n
-        \remark This method is used to implement tactics such as 'revert'. */
-    optional<local_decl> find_local_decl_from_user_name(name const & n) const;
-
-    optional<local_decl> find_last_local_decl() const;
-    local_decl get_last_local_decl() const;
-
-    /** \brief Execute fn for each local declaration created after \c d. */
-    void for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const;
-
-    /** \brief Return a non-none iff other local decls depends on \c d. If the result is not none,
-        then it is the name of the local decl that depends on d.
-        \pre \c d is in this local context. */
-    optional<local_decl> has_dependencies(local_decl const & d, metavar_context const & mctx) const;
-
-    /** \brief Return an unused hypothesis "user name" with the given prefix, the suffix is an
-        unsigned >= idx. */
-    name get_unused_name(name const & prefix, unsigned & idx) const;
-    name get_unused_name(name const & suggestion) const;
-    bool uses_user_name(name const & n) const;
-
-    /** \brief Return true iff all locals in this context are in the set \c ls. */
-    bool is_subset_of(name_set const & ls) const;
-    /** \brief Return true iff all locals in this context are also in \c ctx. */
-    bool is_subset_of(local_context const & ctx) const;
-
-    void pop_local_decl();
-
-    /** \brief Traverse local declarations based on the order they were created */
-    void for_each(std::function<void(local_decl const &)> const & fn) const;
-    optional<local_decl> find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT
-    optional<local_decl> back_find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT
-
-    /** \brief We say a local context is well-formed iff all local declarations only
-        contain local_decl references that were defined before them.
-
-        \remark This method is for debugging purposes. */
-    bool well_formed() const;
-
-    /** \brief Return true iff \c e is well-formed with respect to this local context.
-        That is, all local_decl references in \c e are defined in this context. */
-    bool well_formed(expr const & e) const;
-
-    format pp(formatter const & fmt) const; // NOLINT
-
-    /** \brief Replaced assigned metavariables with their values.
-        This method is a little bit hackish since it reuses the names and ids of
-        the existing local_decls. So, it may affect cached information.
-
-        This method is mainly used in the elaborator for reporting errors,
-        and for instantiating metavariables created by the elaborator before
-        invoking the tactic framework. */
-    local_context instantiate_mvars(metavar_context & ctx) const;
-
-    /** \brief Erase inaccessible annotations from the local context.
-        This function is defined in the file library/equations_compiler/util.h.
-        It is a little bit hackish (like instantiate_mvars) since it reuses the names
-        and ids of existing local_decls. So, it may affect cached information.
-
-        This function is used in the elaborator before invoking the tactic framework. */
-    friend local_context erase_inaccessible_annotations(local_context const & lctx);
-};
-
-/** \brief Return true iff `e` contains a local_decl_ref that contains a value */
-bool contains_let_local_decl(local_context const & lctx, expr const & e);
-
-/** \brief Expand all local_decl_refs (that have values) in `e` */
-expr zeta_expand(local_context const & lctx, expr const & e);
-
-void initialize_local_context();
-void finalize_local_context();
-}
diff --git a/stage0/src/library/local_instances.h b/stage0/src/library/local_instances.h
deleted file mode 100644
index e53dd315f7..0000000000
--- a/stage0/src/library/local_instances.h
+++ /dev/null
@@ -1,29 +0,0 @@
-/*
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-class local_instance {
-    name m_class_name;
-    expr m_local;
-public:
-    local_instance(name const & n, expr const & e):
-        m_class_name(n), m_local(e) {}
-    name const & get_class_name() const { return m_class_name; }
-    expr const & get_local() const { return m_local; }
-    friend bool operator==(local_instance const & l1, local_instance const & l2) {
-        return local_name(l1.m_local) == local_name(l2.m_local);
-    }
-};
-
-inline bool operator!=(local_instance const & l1, local_instance const & l2) {
-    return !(l1 == l2);
-}
-
-typedef list<local_instance> local_instances;
-}
diff --git a/stage0/src/library/metavar_context.cpp b/stage0/src/library/metavar_context.cpp
deleted file mode 100644
index 9bc6b04627..0000000000
--- a/stage0/src/library/metavar_context.cpp
+++ /dev/null
@@ -1,376 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/fresh_name.h"
-#include "util/array_ref.h"
-#include "kernel/abstract.h"
-#include "kernel/for_each_fn.h"
-#include "library/metavar_util.h"
-#include "library/metavar_context.h"
-#include "library/idx_metavar.h"
-
-namespace lean {
-static name *       g_meta_prefix;
-static expr *       g_dummy_type;
-
-extern "C" object * lean_mk_metavar_decl(object * user_name, object * lctx, object * type, object * depth, object * local_insts, uint8 k);
-
-metavar_decl::metavar_decl(name const & user_name, local_context const & lctx, expr const & type):
-    object_ref(lean_mk_metavar_decl(user_name.to_obj_arg(), lctx.to_obj_arg(), type.to_obj_arg(), nat(0).to_obj_arg(), box(0), 0)) {
-}
-
-metavar_decl::metavar_decl():
-    metavar_decl(name(), local_context(), expr()) {}
-
-static expr mk_meta_ref(name const & n) {
-    return mk_metavar(n);
-}
-
-bool is_metavar_decl_ref(level const & u) {
-    return is_mvar(u) && is_prefix_of(*g_meta_prefix, mvar_id(u));
-}
-
-bool is_metavar_decl_ref(expr const & e) {
-    return is_mvar(e) && !is_idx_metavar(e);
-}
-
-name get_metavar_decl_ref_suffix(level const & u) {
-    lean_assert(is_metavar_decl_ref(u));
-    return mvar_id(u).replace_prefix(*g_meta_prefix, name());
-}
-
-name get_metavar_decl_ref_suffix(expr const & e) {
-    lean_assert(is_metavar_decl_ref(e));
-    return mvar_name(e).replace_prefix(*g_meta_prefix, name());
-}
-
-// Hack for interfacing with new DelayedMVarAssignment
-typedef array_ref<expr> array_expr;
-static inline array_expr to_array_expr(exprs const & locals) {
-    buffer<expr> tmp;
-    to_buffer(locals, tmp);
-    return array_expr(tmp);
-}
-
-// Hack for interfacing with new DelayedMVarAssignment
-static inline exprs to_exprs(array_expr const & locals) {
-    exprs r;
-    size_t i = locals.size();
-    while (i > 0) {
-        --i;
-        r = cons(locals[i], r);
-    }
-    return r;
-}
-
-metavar_context::delayed_assignment::delayed_assignment(local_context const & lctx, exprs const & locals, expr const & v):
-    object_ref(mk_cnstr(0, lctx, to_array_expr(locals), v)) {
-}
-
-metavar_context::delayed_assignment::delayed_assignment():
-    delayed_assignment(local_context(), exprs(), expr()) {
-}
-
-exprs metavar_context::delayed_assignment::get_locals() const {
-    return to_exprs(static_cast<array_expr const &>(cnstr_get_ref(raw(), 1)));
-}
-
-// TODO(Leo): fix this
-static name mk_meta_decl_name() {
-    return mk_tagged_fresh_name(*g_meta_prefix);
-}
-
-extern "C" object* lean_mk_metavar_ctx(object*);
-extern "C" object* lean_metavar_ctx_mk_decl(object*, object*, object*, object*, object*, object*, uint8);
-extern "C" object* lean_metavar_ctx_find_decl(object*, object*);
-extern "C" object* lean_metavar_ctx_assign_level(object*, object*, object*);
-extern "C" object* lean_metavar_ctx_assign_expr(object*, object*, object*);
-extern "C" object* lean_metavar_ctx_assign_delayed(object*, object*, object*, object*, object*);
-extern "C" object* lean_metavar_ctx_get_level_assignment(object*, object*);
-extern "C" object* lean_metavar_ctx_get_expr_assignment(object*, object*);
-extern "C" object* lean_metavar_ctx_get_delayed_assignment(object*, object*);
-extern "C" uint8 lean_metavar_ctx_is_level_assigned(object*, object*);
-extern "C" uint8 lean_metavar_ctx_is_expr_assigned(object*, object*);
-extern "C" uint8 lean_metavar_ctx_is_delayed_assigned(object*, object*);
-extern "C" object* lean_metavar_ctx_erase_delayed(object*, object*);
-
-metavar_context::metavar_context():
-    object_ref(lean_mk_metavar_ctx(box(0))) {
-}
-
-bool metavar_context::is_assigned(level const & l) const {
-    lean_assert(is_metavar_decl_ref(l));
-    return lean_metavar_ctx_is_level_assigned(to_obj_arg(), mvar_id(l).to_obj_arg());
-}
-
-bool metavar_context::is_assigned(expr const & m) const {
-    lean_assert(is_metavar_decl_ref(m));
-    return lean_metavar_ctx_is_expr_assigned(to_obj_arg(), mvar_name(m).to_obj_arg());
-}
-
-bool metavar_context::is_delayed_assigned(expr const & m) const {
-    lean_assert(is_metavar_decl_ref(m));
-    return lean_metavar_ctx_is_delayed_assigned(to_obj_arg(), mvar_name(m).to_obj_arg());
-}
-
-level metavar_context::mk_univ_metavar_decl() {
-    // TODO(Leo): should use name_generator
-    return mk_univ_mvar(mk_meta_decl_name());
-}
-
-expr metavar_context::mk_metavar_decl(name const & user_name, local_context const & lctx, expr const & type) {
-    // TODO(Leo): should use name_generator
-    name n = mk_meta_decl_name();
-    m_obj = lean_metavar_ctx_mk_decl(m_obj, n.to_obj_arg(), user_name.to_obj_arg(), lctx.to_obj_arg(), array_mk_empty(), head_beta_reduce(type).to_obj_arg(), false);
-    lean_assert(find_metavar_decl(mk_meta_ref(n)));
-    return mk_meta_ref(n);
-}
-
-optional<metavar_decl> metavar_context::find_metavar_decl(expr const & e) const {
-    lean_assert(is_metavar_decl_ref(e));
-    return to_optional<metavar_decl>(lean_metavar_ctx_find_decl(to_obj_arg(), mvar_name(e).to_obj_arg()));
-}
-
-metavar_decl metavar_context::get_metavar_decl(expr const & e) const {
-    if (auto r = find_metavar_decl(e))
-        return *r;
-    else
-        throw exception("unknown metavariable");
-}
-
-optional<local_decl> metavar_context::find_local_decl(expr const & mvar, name const & n) const {
-    auto mdecl = find_metavar_decl(mvar);
-    if (!mdecl) return optional<local_decl>();
-    return mdecl->get_context().find_local_decl(n);
-}
-
-local_decl metavar_context::get_local_decl(expr const & mvar, name const & n) const {
-    return get_metavar_decl(mvar).get_context().get_local_decl(n);
-}
-
-expr metavar_context::get_local(expr const & mvar, name const & n) const {
-    return get_local_decl(mvar, n).mk_ref();
-}
-
-void metavar_context::assign(level const & u, level const & l) {
-    m_obj = lean_metavar_ctx_assign_level(m_obj, mvar_id(u).to_obj_arg(), l.to_obj_arg());
-    lean_assert(is_assigned(u));
-}
-
-void metavar_context::assign(expr const & e, expr const & v) {
-    lean_assert(!is_delayed_assigned(e));
-    m_obj = lean_metavar_ctx_assign_expr(m_obj, mvar_name(e).to_obj_arg(), v.to_obj_arg());
-    lean_assert(is_assigned(e));
-}
-
-void metavar_context::assign_delayed(expr const & e, local_context const & lctx, exprs const & locals, expr const & v) {
-    m_obj = lean_metavar_ctx_assign_delayed(m_obj, mvar_name(e).to_obj_arg(), lctx.to_obj_arg(), to_array_expr(locals).steal(), v.to_obj_arg());
-    lean_assert(is_delayed_assigned(e));
-}
-
-optional<level> metavar_context::get_assignment(level const & l) const {
-    lean_assert(is_metavar_decl_ref(l));
-    return to_optional<level>(lean_metavar_ctx_get_level_assignment(to_obj_arg(), mvar_id(l).to_obj_arg()));
-}
-
-optional<expr> metavar_context::get_assignment(expr const & e) const {
-    lean_assert(is_metavar_decl_ref(e));
-    return to_optional<expr>(lean_metavar_ctx_get_expr_assignment(to_obj_arg(), mvar_name(e).to_obj_arg()));
-}
-
-optional<metavar_context::delayed_assignment> metavar_context::get_delayed_assignment(expr const & e) const {
-    lean_assert(is_metavar_decl_ref(e));
-    return to_optional<metavar_context::delayed_assignment>(lean_metavar_ctx_get_delayed_assignment(to_obj_arg(), mvar_name(e).to_obj_arg()));
-}
-
-struct metavar_context::interface_impl {
-    metavar_context & m_ctx;
-    /* We store the set of delayed assigned variables that have been found to prevent their values
-       from being visited over and over again. */
-    name_set          m_delayed_found;
-    interface_impl(metavar_context const & ctx):m_ctx(const_cast<metavar_context&>(ctx)) {}
-
-    static bool is_mvar(level const & l) { return is_metavar_decl_ref(l); }
-    bool is_assigned(level const & l) const { return m_ctx.is_assigned(l); }
-    optional<level> get_assignment(level const & l) const { return m_ctx.get_assignment(l); }
-    void assign(level const & u, level const & v) { m_ctx.assign(u, v); }
-
-    static bool is_mvar(expr const & e) { return is_metavar_decl_ref(e); }
-
-    optional<expr> check_delayed_assignment(expr const & e) {
-        lean_assert(is_metavar_decl_ref(e));
-        optional<delayed_assignment> d = m_ctx.get_delayed_assignment(e);
-        if (!d)
-            return none_expr();
-        if (m_delayed_found.contains(mvar_name(e)))
-            return none_expr();
-        /* Remark: a delayed assignment can be transformed in a regular assignment
-           as soon as all metavariables occurring in the assigned value have
-           been assigned. */
-        expr new_v = m_ctx.instantiate_mvars(d->get_val());
-        if (has_expr_metavar(new_v)) {
-            m_delayed_found.insert(mvar_name(e));
-            if (!is_eqp(new_v, d->get_val()))
-                m_ctx.assign_delayed(e, d->get_lctx(), d->get_locals(), new_v);
-            return none_expr();
-        } else {
-            m_ctx.m_obj = lean_metavar_ctx_erase_delayed(m_ctx.m_obj, mvar_name(e).to_obj_arg());
-            lean_assert(!m_ctx.is_delayed_assigned(e));
-            buffer<expr> locals;
-            to_buffer(d->get_locals(), locals);
-            new_v = abstract(new_v, locals.size(), locals.data());
-            unsigned i = locals.size();
-            while (i > 0) {
-                --i;
-                local_decl decl = d->get_lctx().get_local_decl(locals[i]);
-                expr type       = abstract(decl.get_type(), i, locals.data());
-                if (optional<expr> letval = decl.get_value()) {
-                    letval = abstract(*letval, i, locals.data());
-                    new_v  = mk_let(decl.get_user_name(), type, *letval, new_v);
-                } else {
-                    new_v  = mk_lambda(decl.get_user_name(), type, new_v, decl.get_info());
-                }
-            }
-            m_ctx.assign(e, new_v);
-            return some_expr(new_v);
-        }
-    }
-
-    bool is_assigned(expr const & e) const {
-        lean_assert(is_metavar_decl_ref(e));
-        return m_ctx.is_assigned(e) || const_cast<metavar_context::interface_impl*>(this)->check_delayed_assignment(e);
-    }
-
-    optional<expr> get_assignment(expr const & e) const {
-        if (optional<expr> v = m_ctx.get_assignment(e))
-            return v;
-        if (optional<expr> v = const_cast<metavar_context::interface_impl*>(this)->check_delayed_assignment(e))
-            return v;
-        return none_expr();
-    }
-
-    void assign(expr const & m, expr const & v) { m_ctx.assign(m, v); }
-    bool in_tmp_mode() const { return false; }
-};
-
-
-bool metavar_context::has_assigned(level const & l) const {
-    return ::lean::has_assigned(interface_impl(*this), l);
-}
-
-bool metavar_context::has_assigned(expr const & e) const {
-    return ::lean::has_assigned(interface_impl(*this), e);
-}
-
-level metavar_context::instantiate_mvars(level const & l) {
-    interface_impl impl(*this);
-    return ::lean::instantiate_mvars(impl, l);
-}
-
-expr metavar_context::instantiate_mvars(expr const & e) {
-    interface_impl impl(*this);
-    return ::lean::instantiate_mvars(impl, e);
-}
-
-void metavar_context::instantiate_mvars_at_type_of(expr const & m) {
-    metavar_decl d = get_metavar_decl(m);
-    expr type      = d.get_type();
-    expr new_type  = instantiate_mvars(type);
-    if (new_type != type) {
-        m_obj = lean_metavar_ctx_mk_decl(m_obj,
-                                         mvar_name(m).to_obj_arg(),
-                                         d.get_user_name().to_obj_arg(),
-                                         d.get_context().to_obj_arg(),
-                                         array_mk_empty(),
-                                         new_type.to_obj_arg(),
-                                         false);
-    }
-}
-
-template<typename C>
-static bool well_formed_metavar_occs(expr const & e, C const & ds, metavar_context const & ctx) {
-    bool ok = true;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (!ok) return false;
-            if (!has_expr_metavar(e)) return false;
-            if (is_metavar_decl_ref(e)) {
-                if (auto d = ctx.find_metavar_decl(e)) {
-                    if (!d->get_context().is_subset_of(ds)) {
-                        /* invalid metavariable context */
-                        ok = false;
-                        return false;
-                    }
-                } else {
-                    /* undefined metavariable */
-                    ok = false;
-                    return false;
-                }
-            }
-            return true;
-        });
-    return ok;
-}
-
-bool metavar_context::well_formed(local_context const & ctx) const {
-    bool ok = true;
-    name_set visited;
-    ctx.for_each([&](local_decl const & d) {
-            if (!well_formed_metavar_occs(d.get_type(), visited, *this)) {
-                ok = false;
-                lean_unreachable();
-            }
-            if (auto v = d.get_value()) {
-                if (!well_formed_metavar_occs(*v, visited, *this)) {
-                    ok = false;
-                    lean_unreachable();
-                }
-            }
-            visited.insert(d.get_name());
-        });
-    return ok;
-}
-
-bool metavar_context::well_formed(local_context const & ctx, expr const & e) const {
-    return well_formed_metavar_occs(e, ctx, *this);
-}
-
-bool well_formed(local_context const & lctx, metavar_context const & mctx) {
-    if (!lctx.well_formed()) {
-        lean_unreachable();
-        return false;
-    }
-    if (!mctx.well_formed(lctx)) {
-        lean_unreachable();
-        return false;
-    }
-    return true;
-}
-
-bool well_formed(local_context const & lctx, metavar_context const & mctx, expr const & e) {
-    if (!lctx.well_formed(e)) {
-        lean_unreachable();
-        return false;
-    }
-    if (!mctx.well_formed(lctx, e)) {
-        lean_unreachable();
-        return false;
-    }
-    return true;
-}
-
-void initialize_metavar_context() {
-    g_meta_prefix = new name("_mlocal");
-    mark_persistent(g_meta_prefix->raw());
-    register_name_generator_prefix(*g_meta_prefix);
-    g_dummy_type  = new expr(mk_constant(name::mk_internal_unique_name()));
-    mark_persistent(g_dummy_type->raw());
-}
-
-void finalize_metavar_context() {
-    delete g_meta_prefix;
-    delete g_dummy_type;
-}
-}
diff --git a/stage0/src/library/metavar_context.h b/stage0/src/library/metavar_context.h
deleted file mode 100644
index ddd642a75b..0000000000
--- a/stage0/src/library/metavar_context.h
+++ /dev/null
@@ -1,141 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/local_context.h"
-
-namespace lean {
-class metavar_decl : public object_ref {
-public:
-    metavar_decl();
-    metavar_decl(name const & user_name, local_context const & ctx, expr const & type);
-    metavar_decl(metavar_decl const & other):object_ref(other) {}
-    metavar_decl(metavar_decl && other):object_ref(other) {}
-    metavar_decl(obj_arg o):object_ref(o) {}
-    metavar_decl(b_obj_arg o, bool):object_ref(o, true) {}
-    metavar_decl & operator=(metavar_decl const & other) { object_ref::operator=(other); return *this; }
-    metavar_decl & operator=(metavar_decl && other) { object_ref::operator=(other); return *this; }
-    name const & get_user_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 0)); }
-    local_context const & get_context() const { return static_cast<local_context const &>(cnstr_get_ref(raw(), 1)); }
-    expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 2)); }
-};
-
-bool is_metavar_decl_ref(level const & l);
-bool is_metavar_decl_ref(expr const & e);
-
-name get_metavar_decl_ref_suffix(level const & l);
-name get_metavar_decl_ref_suffix(expr const & e);
-
-class metavar_context : public object_ref {
-    class delayed_assignment : public object_ref {
-    public:
-        delayed_assignment();
-        delayed_assignment(local_context const & lctx, exprs const & locals, expr const & v);
-        delayed_assignment(delayed_assignment const & other):object_ref(other) {}
-        delayed_assignment(delayed_assignment && other):object_ref(other) {}
-        delayed_assignment(obj_arg o):object_ref(o) {}
-        delayed_assignment(b_obj_arg o, bool):object_ref(o, true) {}
-        delayed_assignment & operator=(delayed_assignment const & other) { object_ref::operator=(other); return *this; }
-        delayed_assignment & operator=(delayed_assignment && other) { object_ref::operator=(other); return *this; }
-        local_context const & get_lctx() const { return static_cast<local_context const &>(cnstr_get_ref(raw(), 0)); }
-        exprs get_locals() const;
-        expr const & get_val() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 2)); }
-    };
-    struct interface_impl;
-    friend struct interface_impl;
-public:
-    metavar_context();
-    explicit metavar_context(obj_arg o):object_ref(o) {}
-    metavar_context(b_obj_arg o, bool):object_ref(o, true) {}
-    metavar_context(metavar_context const & other):object_ref(other) {}
-    metavar_context(metavar_context && other):object_ref(other) {}
-    metavar_context & operator=(metavar_context const & other) { object_ref::operator=(other); return *this; }
-    metavar_context & operator=(metavar_context && other) { object_ref::operator=(other); return *this; }
-
-    level mk_univ_metavar_decl();
-
-    expr mk_metavar_decl(name const & user_name, local_context const & ctx, expr const & type);
-
-    expr mk_metavar_decl(local_context const & ctx, expr const & type) {
-        return mk_metavar_decl(name(), ctx, type);
-    }
-
-    optional<metavar_decl> find_metavar_decl(expr const & mvar) const;
-
-    metavar_decl get_metavar_decl(expr const & mvar) const;
-
-    /** \brief Return the local_decl for `n` in the local context for the metavariable `mvar`
-        \pre is_metavar(mvar) */
-    optional<local_decl> find_local_decl(expr const & mvar, name const & n) const;
-
-    local_decl get_local_decl(expr const & mvar, name const & n) const;
-
-    /** \brief Return the local_decl_ref for `n` in the local context for the metavariable `mvar`
-
-        \pre is_metavar(mvar)
-        \pre find_metavar_decl(mvar)
-        \pre find_metavar_decl(mvar)->get_context().get_local_decl(n) */
-    expr get_local(expr const & mvar, name const & n) const;
-
-    bool is_assigned(level const & l) const;
-    bool is_assigned(expr const & m) const;
-    bool is_delayed_assigned(expr const & m) const;
-
-    void assign(level const & u, level const & l);
-    void assign(expr const & e, expr const & v);
-    /*
-      Add the delayed assignment
-      ```
-      e := Fun(locals, v)
-      ```
-      This kind of assignment is created by the `intro` tactic.
-      The term `v` contains metavariables that have not been instantiated yet.
-      So, `abstract_locals(locals, v)` would not work correctly.
-      We also cannot create an auxiliary metavariable in this case since it would "solve" the new goal
-      created by the `intro` tactic.
-
-      \pre is_metavar_decl_ref(e)
-    */
-    void assign_delayed(expr const & e, local_context const & lctx, exprs const & locals, expr const & v);
-
-    level instantiate_mvars(level const & l);
-    expr instantiate_mvars(expr const & e);
-
-    bool has_assigned(level const & l) const;
-    bool has_assigned(levels const & ls) const;
-    bool has_assigned(expr const & e) const;
-
-    optional<level> get_assignment(level const & l) const;
-    optional<expr> get_assignment(expr const & e) const;
-    optional<delayed_assignment> get_delayed_assignment(expr const & e) const;
-
-    /** \brief Instantiate the assigned meta-variables in the type of \c m
-        \pre get_metavar_decl(m) is not none */
-    void instantiate_mvars_at_type_of(expr const & m);
-
-    /** \brief Return true iff \c ctx is well-formed with respect to this metavar context.
-        That is, every metavariable ?M occurring in \c ctx is declared here, and
-        for every metavariable ?M occurring in a declaration \c d, the context of ?M
-        must be a subset of the declarations declared *before* \c d.
-
-        \remark This method is used for debugging purposes. */
-    bool well_formed(local_context const & ctx) const;
-
-    /** \brief Return true iff all metavariables ?M in \c e are declared in this metavar context,
-        and context of ?M is a subset of \c ctx */
-    bool well_formed(local_context const & ctx, expr const & e) const;
-};
-
-/** \brief Check whether the local context lctx is well-formed and well-formed with respect to \c mctx.
-    \remark This procedure is used for debugging purposes. */
-bool well_formed(local_context const & lctx, metavar_context const & mctx);
-
-/** \brief Check whether \c e is well-formed with respect to \c lctx and \c mctx. */
-bool well_formed(local_context const & lctx, metavar_context const & mctx, expr const & e);
-
-void initialize_metavar_context();
-void finalize_metavar_context();
-}
diff --git a/stage0/src/library/metavar_util.h b/stage0/src/library/metavar_util.h
deleted file mode 100644
index ed6979d2fe..0000000000
--- a/stage0/src/library/metavar_util.h
+++ /dev/null
@@ -1,199 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/instantiate.h"
-#include "library/replace_visitor.h"
-
-namespace lean {
-/*
-Helper functions for metavariable assignments.
-The template parameter CTX must be an object that
-provides the following API:
-
-bool is_mvar(level const & l) const;
-bool is_assigned(level const & l) const;
-optional<level> get_assignment(level const & l) const;
-void assign(level const & u, level const & v);
-
-bool is_mvar(expr const & e) const;
-bool is_assigned(expr const & e) const;
-optional<expr> get_assignment(expr const & e) const;
-void assign(expr const & m, expr const & v);
-
-bool in_tmp_mode() const;
-*/
-
-template<typename CTX>
-bool has_assigned(CTX const & ctx, level const & l) {
-    if (!has_mvar(l))
-        return false;
-    bool found = false;
-    for_each(l, [&](level const & l) {
-            if (!has_mvar(l))
-                return false; // stop search
-            if (found)
-                return false;  // stop search
-            if (ctx.is_mvar(l) && ctx.is_assigned(l)) {
-                found = true;
-                return false; // stop search
-            }
-            return true; // continue search
-        });
-    return found;
-}
-
-template<typename CTX>
-bool has_assigned(CTX const & ctx, levels const & ls) {
-    for (level const & l : ls) {
-        if (has_assigned(ctx, l))
-            return true;
-    }
-    return false;
-}
-
-template<typename CTX>
-bool has_assigned(CTX const & ctx, expr const & e) {
-    if (!has_expr_metavar(e) && !has_univ_metavar(e))
-        return false;
-    bool found = false;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (!has_expr_metavar(e) && !has_univ_metavar(e))
-                return false; // stop search
-            if (found)
-                return false; // stop search
-            if ((ctx.is_mvar(e) && ctx.is_assigned(e)) ||
-                (is_constant(e) && has_assigned(ctx, const_levels(e))) ||
-                (is_sort(e) && has_assigned(ctx, sort_level(e)))) {
-                found = true;
-                return false; // stop search
-            }
-            if (is_metavar(e))
-                return false; // do not search type
-            return true; // continue search
-        });
-    return found;
-}
-
-template<typename CTX>
-level instantiate_mvars(CTX & ctx, level const & l) {
-    if (!has_assigned(ctx, l))
-        return l;
-    return replace(l, [&](level const & l) {
-            if (!has_mvar(l)) {
-                return some_level(l);
-            } else if (ctx.is_mvar(l)) {
-                if (auto v1 = ctx.get_assignment(l)) {
-                    level v2 = instantiate_mvars(ctx, *v1);
-                    if (*v1 != v2) {
-                        if (!ctx.in_tmp_mode())
-                            ctx.assign(l, v2);
-                        return some_level(v2);
-                    } else {
-                        return some_level(*v1);
-                    }
-                }
-            }
-            return none_level();
-        });
-}
-
-template<typename CTX>
-class instantiate_mvars_fn : public replace_visitor {
-    CTX & m_ctx;
-
-    level visit_level(level const & l) {
-        return instantiate_mvars(m_ctx, l);
-    }
-
-    levels visit_levels(levels const & ls) {
-        return map_reuse(ls, [&](level const & l) { return visit_level(l); });
-    }
-
-    virtual expr visit_sort(expr const & s) override {
-        return update_sort(s, visit_level(sort_level(s)));
-    }
-
-    virtual expr visit_constant(expr const & c) override {
-        return update_constant(c, visit_levels(const_levels(c)));
-    }
-
-    virtual expr visit_local(expr const & e) override {
-        return update_local(e, visit(local_type(e)));
-    }
-
-    virtual expr visit_meta(expr const & m) override {
-        if (m_ctx.is_mvar(m)) {
-            if (auto v1 = m_ctx.get_assignment(m)) {
-                if (!has_metavar(*v1)) {
-                    return *v1;
-                } else {
-                    expr v2 = visit(*v1);
-                    if (!m_ctx.in_tmp_mode() && v2 != *v1)
-                        m_ctx.assign(m, v2);
-                    return v2;
-                }
-            } else {
-                return m;
-            }
-        } else {
-            return m;
-        }
-    }
-
-    virtual expr visit_app(expr const & e) override {
-        buffer<expr> args;
-        expr const & f = get_app_rev_args(e, args);
-        if (m_ctx.is_mvar(f)) {
-            if (auto v = m_ctx.get_assignment(f)) {
-                expr new_app = apply_beta(*v, args.size(), args.data());
-                if (has_metavar(new_app))
-                    return visit(new_app);
-                else
-                    return new_app;
-            }
-        }
-        expr new_f = visit(f);
-        buffer<expr> new_args;
-        bool modified = !is_eqp(new_f, f);
-        for (expr const & arg : args) {
-            expr new_arg = visit(arg);
-            if (!is_eqp(arg, new_arg))
-                modified = true;
-            new_args.push_back(new_arg);
-        }
-        if (!modified)
-            return e;
-        else
-            return mk_rev_app(new_f, new_args);
-    }
-
-    virtual expr visit_mdata(expr const & e) override {
-        return update_mdata(e, visit(mdata_expr(e)));
-    }
-
-    virtual expr visit(expr const & e) override {
-        if (!has_expr_metavar(e) && !has_univ_metavar(e))
-            return e;
-        else
-            return replace_visitor::visit(e);
-    }
-
-public:
-    instantiate_mvars_fn(CTX & ctx):m_ctx(ctx) {}
-    expr operator()(expr const & e) {
-        return visit(e);
-    }
-};
-
-template<typename CTX>
-expr instantiate_mvars(CTX & ctx, expr const & e) {
-    if (!has_assigned(ctx, e))
-        return e;
-    expr r = instantiate_mvars_fn<CTX>(ctx)(e);
-    lean_assert(!has_assigned(ctx, r));
-    return r;
-}
-}
diff --git a/stage0/src/library/type_context.cpp b/stage0/src/library/type_context.cpp
index 3ec1d22620..9110b17715 100644
--- a/stage0/src/library/type_context.cpp
+++ b/stage0/src/library/type_context.cpp
@@ -18,11 +18,9 @@ Author: Leonardo de Moura
 #include "library/class.h"
 #include "library/pp_options.h"
 #include "library/annotation.h"
-#include "library/idx_metavar.h"
 #include "library/reducible.h"
 #include "library/suffixes.h"
 #include "library/constants.h"
-#include "library/metavar_util.h"
 #include "library/exception.h"
 #include "library/type_context.h"
 #include "library/locals.h"
@@ -33,54 +31,17 @@ Author: Leonardo de Moura
 
 namespace lean {
 
-/* =====================
-   type_context_old::tmp_locals
-   ===================== */
-type_context_old::tmp_locals::~tmp_locals() {
-    for (unsigned i = 0; i < m_locals.size(); i++)
-        m_ctx.pop_local();
-}
-
 /* =====================
    type_context_old
    ===================== */
 
-type_context_old::type_context_old(environment const & env, options const &, metavar_context const & mctx,
-                                   local_context const & lctx, transparency_mode):
-    m_env(env),
-    m_mctx(mctx), m_lctx(lctx) {
+type_context_old::type_context_old(environment const & env, options const &, transparency_mode):
+    m_env(env) {
 }
 
 type_context_old::~type_context_old() {
 }
 
-/** \brief Helper class for pretty printing terms that contain local_decl_ref's and metavar_decl_ref's */
-class pp_ctx {
-    type_context_old m_ctx;
-    formatter    m_fmt;
-public:
-    pp_ctx(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx):
-        m_ctx(env, opts, mctx, lctx),
-        m_fmt(get_global_ios().get_formatter_factory()(env, opts, m_ctx)) {}
-    format pp(expr const & e) {
-        return m_fmt(m_ctx.instantiate_mvars(e));
-    }
-};
-
-std::function<format(expr const &)>
-mk_pp_ctx(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx) {
-    auto pp_fn = std::make_shared<pp_ctx>(env, opts, mctx, lctx);
-    return [=](expr const & e) { // NOLINT
-        metavar_context mctx_tmp(mctx);
-        return pp_fn->pp(mctx_tmp.instantiate_mvars(e));
-    };
-}
-
-std::function<format(expr const &)>
-mk_pp_ctx(type_context_old const & ctx) {
-    return mk_pp_ctx(ctx.env(), ctx.get_options(), ctx.mctx(), ctx.lctx());
-}
-
 void initialize_type_context() {
 }
 
diff --git a/stage0/src/library/type_context.h b/stage0/src/library/type_context.h
index 4d4466e611..586ccea0a2 100644
--- a/stage0/src/library/type_context.h
+++ b/stage0/src/library/type_context.h
@@ -11,13 +11,10 @@ Author: Leonardo de Moura
 #include "util/lbool.h"
 #include "util/fresh_name.h"
 #include "kernel/environment.h"
-#include "library/idx_metavar.h"
 #include "library/projection.h"
-#include "library/metavar_context.h"
 #include "library/abstract_type_context.h"
 #include "library/exception.h"
 #include "library/expr_pair.h"
-#include "library/local_instances.h"
 
 namespace lean {
 enum class transparency_mode { All = 0, Semireducible, Reducible };
@@ -51,37 +48,11 @@ class type_context_old : public abstract_type_context {
     typedef buffer<optional<level>> tmp_uassignment;
     typedef buffer<expr>            tmp_etype;
     typedef buffer<optional<expr>>  tmp_eassignment;
-    typedef buffer<metavar_context> mctx_stack;
     enum class tmp_trail_kind { Level, Expr };
     typedef buffer<pair<tmp_trail_kind, unsigned>> tmp_trail;
     friend struct instance_synthesizer;
-    struct scope_data {
-        metavar_context m_mctx;
-        unsigned        m_tmp_uassignment_sz;
-        unsigned        m_tmp_eassignment_sz;
-        unsigned        m_tmp_trail_sz;
-        scope_data(metavar_context const & mctx, unsigned usz, unsigned esz, unsigned tsz):
-            m_mctx(mctx), m_tmp_uassignment_sz(usz), m_tmp_eassignment_sz(esz), m_tmp_trail_sz(tsz) {}
-    };
-public:
-    struct tmp_data {
-        tmp_uassignment & m_uassignment;
-        tmp_etype       & m_etype;
-        tmp_eassignment & m_eassignment;
-        /* m_tmp_mvar_local_context contains m_lctx when tmp mode is activated.
-           This is the context for all temporary meta-variables. */
-        local_context     m_mvar_lctx;
-        /* undo/trail stack for m_tmp_uassignment/m_tmp_eassignment */
-        tmp_trail         m_trail;
-        tmp_data(tmp_uassignment & uassignment, tmp_etype & etype, tmp_eassignment & eassignment, local_context const & lctx):
-            m_uassignment(uassignment), m_etype(etype), m_eassignment(eassignment), m_mvar_lctx(lctx) {}
-    };
 private:
-    typedef buffer<scope_data> scopes;
     environment        m_env;
-    metavar_context    m_mctx;
-    local_context      m_lctx;
-    local_instances    m_local_instances;
     /* We only cache results when m_used_assignment is false */
     bool               m_used_assignment{false};
     transparency_mode  m_transparency_mode;
@@ -90,8 +61,6 @@ private:
     /* m_is_def_eq_depth is only used for tracing purposes */
     unsigned           m_is_def_eq_depth{0};
     /* Stack of backtracking point (aka scope) */
-    scopes             m_scopes;
-    tmp_data *         m_tmp_data{nullptr};
     /* Higher-order unification approximation options.
 
        Modules that use approximations:
@@ -147,15 +116,9 @@ private:
     optional<expr> reduce_projection_core(optional<projection_info> const & info, expr const & e);
 
 public:
-    type_context_old(environment const & env, options const & o, metavar_context const & mctx, local_context const & lctx,
-                 transparency_mode m = transparency_mode::Reducible);
-    type_context_old(environment const & env, options const & o, local_context const & lctx,
-                     transparency_mode m = transparency_mode::Reducible):
-        type_context_old(env, o, metavar_context(), lctx, m) {}
+    type_context_old(environment const & env, options const & o, transparency_mode m = transparency_mode::Reducible);
     explicit type_context_old(environment const & env, transparency_mode m = transparency_mode::Reducible):
-        type_context_old(env, options(), metavar_context(), local_context(), m) {}
-    type_context_old(environment const & env, options const & o, transparency_mode m = transparency_mode::Reducible):
-        type_context_old(env, o, metavar_context(), local_context(), m) {}
+        type_context_old(env, options(), m) {}
     virtual ~type_context_old();
 
     type_context_old & operator=(type_context_old const &) = delete;
@@ -167,28 +130,11 @@ public:
     // TODO(Leo): avoid ::lean::mk_fresh_name
     virtual name next_name() override { return ::lean::mk_fresh_name(); }
 
-    virtual optional<name> get_local_pp_name(expr const & e) override {
-        if (optional<local_decl> decl = m_lctx.find_local_decl(e)) {
-            return optional<name>(decl->get_user_name());
-        }
-        return optional<name>();
+    virtual optional<name> get_local_pp_name(expr const &) override {
+        lean_unreachable();
     }
 
 
-    virtual local_context const & lctx() const override { return m_lctx; }
-    virtual metavar_context const & mctx() const override { return m_mctx; }
-    expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
-    expr mk_metavar_decl(name const & pp_n, local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(pp_n, ctx, type); }
-    optional<metavar_decl> find_metavar_decl(expr const & mvar) const { return m_mctx.find_metavar_decl(mvar); }
-
-    level mk_univ_metavar_decl() { return m_mctx.mk_univ_metavar_decl(); }
-
-    name get_unused_name(name const & prefix, unsigned & idx) const { return m_lctx.get_unused_name(prefix, idx); }
-    name get_unused_name(name const & suggestion) const { return m_lctx.get_unused_name(suggestion); }
-
-    /* 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);
 
     /* Store the current local instances in the local context.
@@ -233,7 +179,6 @@ public:
     }
 
     virtual bool is_def_eq(expr const &, expr const &) override { lean_unreachable(); }
-    bool is_def_eq_at(local_context const & lctx, expr const & a, expr const & b);
 
     bool match(expr const & e1, expr const & e2) {
         flet<bool> update_left(m_update_left, true);
@@ -325,13 +270,6 @@ public:
     */
     expr revert(buffer<expr> & locals, expr const & mvar, bool preserve_locals_order);
 
-    expr mk_lambda(local_context const & lctx, buffer<expr> const & locals, expr const & e);
-    expr mk_pi(local_context const & lctx, buffer<expr> const & locals, expr const & e);
-    expr mk_lambda(local_context const & lctx, expr const & local, expr const & e);
-    expr mk_pi(local_context const & lctx, expr const & local, expr const & e);
-    expr mk_lambda(local_context const & lctx, std::initializer_list<expr> const & locals, expr const & e);
-    expr mk_pi(local_context const & lctx, std::initializer_list<expr> const & locals, expr const & e);
-
     expr mk_lambda(buffer<expr> const & locals, expr const & e);
     expr mk_pi(buffer<expr> const & locals, expr const & e);
     expr mk_lambda(expr const & local, expr const & e);
@@ -349,7 +287,6 @@ public:
     optional<expr> mk_class_instance(expr const & type);
     optional<expr> mk_subsingleton_instance(expr const & type);
     /* Create type class instance in a different local context */
-    optional<expr> mk_class_instance_at(local_context const & lctx, expr const & type);
 
     transparency_mode mode() const { return m_transparency_mode; }
     unsigned mode_idx() const { return static_cast<unsigned>(mode()); }
@@ -413,33 +350,6 @@ public:
        It is used when performing type class resolution and matching.
        -------------------------- */
 public:
-    struct tmp_mode_scope {
-        type_context_old &      m_ctx;
-        buffer<optional<level>> m_tmp_uassignment;
-        buffer<expr>            m_tmp_etype;
-        buffer<optional<expr>>  m_tmp_eassignment;
-        tmp_data *              m_old_data;
-        tmp_data                m_data;
-        tmp_mode_scope(type_context_old & ctx):
-            m_ctx(ctx), m_old_data(ctx.m_tmp_data), m_data(m_tmp_uassignment, m_tmp_etype, m_tmp_eassignment, ctx.lctx()) {
-            m_ctx.m_tmp_data = &m_data;
-        }
-        ~tmp_mode_scope() {
-            m_ctx.m_tmp_data = m_old_data;
-        }
-    };
-    struct tmp_mode_scope_with_data {
-        type_context_old & m_ctx;
-        tmp_data *     m_old_data;
-        tmp_mode_scope_with_data(type_context_old & ctx, tmp_data & data):
-            m_ctx(ctx), m_old_data(ctx.m_tmp_data) {
-            m_ctx.m_tmp_data = &data;
-        }
-        ~tmp_mode_scope_with_data() {
-            m_ctx.m_tmp_data = m_old_data;
-        }
-    };
-    bool in_tmp_mode() const { return m_tmp_data != nullptr; }
     optional<level> get_tmp_uvar_assignment(unsigned idx) const;
     optional<expr> get_tmp_mvar_assignment(unsigned idx) const;
     optional<level> get_tmp_assignment(level const & l) const;
@@ -478,12 +388,6 @@ private:
     optional<constant_info> get_decl(name const &) { lean_unreachable(); }
 
 private:
-    pair<local_context, expr> revert_core(buffer<expr> & to_revert, local_context const & ctx,
-                                          expr const & type, bool preserve_to_revert_order);
-    expr revert_core(buffer<expr> & to_revert, expr const & mvar, bool preserve_to_revert_order);
-    expr elim_mvar_deps(expr const & e, unsigned num, expr const * locals);
-    expr mk_binding(bool is_pi, local_context const & lctx, unsigned num_locals, expr const * locals, expr const & e);
-
     /* ------------
        Temporary metavariable assignment.
        ------------ */
@@ -497,9 +401,6 @@ public:
     bool is_mvar(level const & l) const;
     /* Return true iff `e` is a regular or temporary metavar */
     bool is_mvar(expr const & e) const;
-    bool is_regular_mvar(expr const & e) const { return is_metavar_decl_ref(e); }
-    bool is_tmp_mvar(level const & l) const { return is_idx_metauniv(l); }
-    bool is_tmp_mvar(expr const & e) const { return is_idx_metavar(e); }
     /* Return true iff
        1- `l` is a temporary universe metavariable and type_context_old is in tmp mode, OR
        2- `l` is a regular universe metavariable an type_context_old is not in tmp_mode. */
@@ -519,9 +420,6 @@ public:
     expr instantiate_mvars(expr const &) { lean_unreachable(); }
     /** \brief Instantiate the assigned meta-variables in the type of \c m
         \pre get_metavar_decl(m) is not none */
-    void instantiate_mvars_at_type_of(expr const & m) {
-        m_mctx.instantiate_mvars_at_type_of(m);
-    }
     /** Set the number of tmp metavars.
         \pre in_tmp_mode() */
     void resize_tmp_mvars(unsigned new_sz = 0);
@@ -664,16 +562,6 @@ public:
     friend class tmp_locals;
 };
 
-/** Create a formatting function that can 'decode' metavar_decl_refs and local_decl_refs
-    with declarations stored in mctx and lctx */
-std::function<format(expr const &)>
-mk_pp_ctx(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx);
-
-/** Create a formatting function that can 'decode' metavar_decl_refs and local_decl_refs
-    with declarations stored in ctx */
-std::function<format(expr const &)>
-mk_pp_ctx(type_context_old const & ctx);
-
 void initialize_type_context();
 void finalize_type_context();
 }
diff --git a/stage0/src/library/util.h b/stage0/src/library/util.h
index 2a071bbe00..5f8b201d51 100644
--- a/stage0/src/library/util.h
+++ b/stage0/src/library/util.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/environment.h"
 #include "library/expr_pair.h"
+#include "library/abstract_type_context.h"
 
 namespace lean {
 /* If \c n is not in \c env, then return \c. Otherwise, find the first j >= idx s.t.