diff --git a/src/compiler/util.cpp b/src/compiler/util.cpp
index a52fb1b57c..c3d091c408 100644
--- a/src/compiler/util.cpp
+++ b/src/compiler/util.cpp
@@ -25,7 +25,7 @@ static bool is_typeformer_app(buffer<name> const & typeformer_names, expr const
 
 void get_rec_args(environment const & env, name const & n, buffer<buffer<bool>> & r) {
     lean_assert(inductive::is_inductive_decl(env, n));
-    type_checker tc(env);
+    old_type_checker tc(env);
     declaration ind_decl   = env.get(n);
     declaration rec_decl   = env.get(inductive::get_elim_name(n));
     unsigned nparams       = *inductive::get_num_params(env, n);
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 957e936158..cec213f227 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -150,7 +150,7 @@ environment eval_cmd(parser & p) {
         auto tc = mk_type_checker(p.env());
         r = tc->whnf(e).first;
     } else {
-        type_checker tc(p.env());
+        old_type_checker tc(p.env());
         bool eta = false;
         bool eval_nested_prop = false;
         r = normalize(tc, ls, e, eta, eval_nested_prop);
diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp
index e6c19bf232..29a1e8737a 100644
--- a/src/frontends/lean/coercion_elaborator.cpp
+++ b/src/frontends/lean/coercion_elaborator.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/fresh_name.h"
-#include "kernel/type_checker.h"
 #include "kernel/metavar.h"
 #include "kernel/constraint.h"
 #include "kernel/instantiate.h"
@@ -13,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/coercion.h"
 #include "library/unifier.h"
 #include "library/choice_iterator.h"
+#include "library/old_type_checker.h"
 #include "frontends/lean/coercion_elaborator.h"
 
 namespace lean {
@@ -24,7 +24,7 @@ coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr cons
     lean_assert(use_id  || length(m_coercions)     == length(m_choices));
 }
 
-list<expr> get_coercions_from_to(type_checker & from_tc, type_checker & to_tc,
+list<expr> get_coercions_from_to(old_type_checker & from_tc, old_type_checker & to_tc,
                                  expr const & from_type, expr const & to_type, constraint_seq & cs, bool lift_coe) {
     constraint_seq new_cs;
     environment const & env = to_tc.env();
@@ -93,7 +93,7 @@ bool is_pi_meta(expr const & e) {
 
 /** \brief Given a term <tt>a : a_type</tt>, and a metavariable \c m, creates a constraint
     that considers coercions from a_type to the type assigned to \c m. */
-constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coercion_info_manager & infom,
+constraint mk_coercion_cnstr(old_type_checker & from_tc, old_type_checker & to_tc, coercion_info_manager & infom,
                              expr const & m, expr const & a, expr const & a_type,
                              justification const & j, unsigned delay_factor, bool lift_coe) {
     auto choice_fn = [=, &from_tc, &to_tc, &infom](expr const & meta, expr const & d_type, substitution const & s) {
diff --git a/src/frontends/lean/coercion_elaborator.h b/src/frontends/lean/coercion_elaborator.h
index 2e296d94b0..47d5beddb1 100644
--- a/src/frontends/lean/coercion_elaborator.h
+++ b/src/frontends/lean/coercion_elaborator.h
@@ -43,11 +43,11 @@ bool is_pi_meta(expr const & e);
 
     \see coercion_info_manager
 */
-constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coercion_info_manager & infom,
+constraint mk_coercion_cnstr(old_type_checker & from_tc, old_type_checker & to_tc, coercion_info_manager & infom,
                              expr const & m, expr const & a, expr const & a_type,
                              justification const & j, unsigned delay_factor, bool lift_coe);
 
-list<expr> get_coercions_from_to(type_checker & from_tc, type_checker & to_tc,
+list<expr> get_coercions_from_to(old_type_checker & from_tc, old_type_checker & to_tc,
                                  expr const & from_type, expr const & to_type, constraint_seq & cs,
                                  bool lift_coe);
 }
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index cda65d513b..84134cf116 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -107,14 +107,14 @@ static bool save_error(pos_info_provider const * pip, expr const & e) {
     return g_elaborator_reported_errors->save(pip, e);
 }
 
-type_checker_ptr mk_coercion_from_type_checker(environment const & env) {
+old_type_checker_ptr mk_coercion_from_type_checker(environment const & env) {
     auto irred_pred = mk_irreducible_pred(env);
     return mk_type_checker(env, [=](name const & n) {
             return has_coercions_from(env, n) || irred_pred(n);
         });
 }
 
-type_checker_ptr mk_coercion_to_type_checker(environment const & env) {
+old_type_checker_ptr mk_coercion_to_type_checker(environment const & env) {
     auto irred_pred = mk_irreducible_pred(env);
     return mk_type_checker(env, [=](name const & n) {
             return has_coercions_to(env, n) || irred_pred(n);
@@ -305,7 +305,7 @@ void elaborator::erase_coercion_info(expr const & e) {
 void elaborator::instantiate_info(substitution s) {
     if (m_to_show_hole) {
         expr meta      = s.instantiate(*m_to_show_hole);
-        expr meta_type = s.instantiate(type_checker(env()).infer(meta).first);
+        expr meta_type = s.instantiate(old_type_checker(env()).infer(meta).first);
         goal g(meta, meta_type);
         proof_state ps(goals(g), s, constraints());
         auto out = regular(env(), ios(), m_tc->get_type_context());
@@ -441,7 +441,7 @@ static bool is_implicit_pi(expr const & e) {
 
 /** \brief Auxiliary function for adding implicit arguments to coercions to function-class */
 expr elaborator::add_implict_args(expr e, constraint_seq & cs) {
-    type_checker & tc = *m_tc;
+    old_type_checker & tc = *m_tc;
     constraint_seq new_cs;
     expr type = tc.whnf(tc.infer(e, new_cs), new_cs);
     if (!is_implicit_pi(type))
@@ -1015,7 +1015,7 @@ enum lhs_meta_kind { None, Accessible, Inaccessible };
 
    \remark If the lhs contains accessible and inaccessible metavariables, an accessible is returned.
 */
-static pair<lhs_meta_kind, expr> find_lhs_meta(type_checker & tc, expr const & e) {
+static pair<lhs_meta_kind, expr> find_lhs_meta(old_type_checker & tc, expr const & e) {
     if (!has_metavar(e))
         return mk_pair(None, expr());
     environment const & env = tc.env();
@@ -1116,7 +1116,7 @@ static pair<lhs_meta_kind, expr> find_lhs_meta(type_checker & tc, expr const & e
     (λ (ideq : ∀ {A : Type} {a b : A}, @eq A a b → @eq A a b) (x_1 : Type) (x_2 x_3 : x_1) (H : @eq x_1 x_2 x_3),
        [equation (@ideq x_1 x_2 x_3 H) H])]
 */
-static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) {
+static expr assign_equation_lhs_metas(old_type_checker & tc, expr const & eqns) {
     lean_assert(is_equations(eqns));
     if (!has_metavar(eqns))
         return eqns;
@@ -1210,7 +1210,7 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
         if (display_unassigned_mvars(new_eqns, new_s)) {
             return lazy_list<constraints>();
         }
-        type_checker_ptr tc = mk_type_checker(_env);
+        old_type_checker_ptr tc = mk_type_checker(_env);
         new_eqns            = assign_equation_lhs_metas(*tc, new_eqns);
         expr val            = compile_equations(*tc, _ios, new_eqns, meta, meta_type);
         justification j     = mk_justification("equation compilation", some_expr(eqns));
@@ -1361,7 +1361,7 @@ expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
     expr dec_proof      = visit(decreasing_proof(e), cs);
     expr f_type         = mlocal_type(get_app_fn(*m_equation_lhs));
     buffer<expr> ts;
-    type_checker & tc = *m_tc;
+    old_type_checker & tc = *m_tc;
     to_telescope(tc, f_type, ts, optional<binder_info>(), cs);
     buffer<expr> old_args;
     buffer<expr> new_args;
@@ -2226,7 +2226,7 @@ bool elaborator::display_unassigned_mvars(expr const & e, substitution const & s
         visit_unassigned_mvars(e, [&](expr const & mvar) {
                 if (auto it = mvar_to_meta(mvar)) {
                     expr meta      = tmp_s.instantiate(*it);
-                    expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first);
+                    expr meta_type = tmp_s.instantiate(old_type_checker(env()).infer(meta).first);
                     goal g(meta, meta_type);
                     proof_state ps(goals(g), s, constraints());
                     display_unsolved_proof_state(mvar, ps, "don't know how to synthesize placeholder");
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 0e17305b70..fd9e9915e2 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -9,12 +9,12 @@ Author: Leonardo de Moura
 #include <vector>
 #include "util/list.h"
 #include "kernel/metavar.h"
-#include "kernel/type_checker.h"
 #include "library/expr_lt.h"
 #include "library/unifier.h"
 #include "library/old_local_context.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/elaborate.h"
+#include "library/old_type_checker.h"
 #include "frontends/lean/elaborator_context.h"
 #include "frontends/lean/coercion_elaborator.h"
 #include "frontends/lean/util.h"
@@ -30,9 +30,9 @@ class elaborator : public coercion_info_manager {
     typedef rb_map<expr, pair<expr, constraint_seq>, expr_quick_cmp> cache;
     typedef std::vector<pair<expr, expr>> to_check_sorts;
     elaborator_context & m_ctx;
-    type_checker_ptr     m_tc;
-    type_checker_ptr     m_coercion_from_tc;
-    type_checker_ptr     m_coercion_to_tc;
+    old_type_checker_ptr     m_tc;
+    old_type_checker_ptr     m_coercion_from_tc;
+    old_type_checker_ptr     m_coercion_to_tc;
     // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
     // representing the context where ?m was created.
     old_local_context    m_context; // current local context: a list of local constants
diff --git a/src/frontends/lean/find_cmd.cpp b/src/frontends/lean/find_cmd.cpp
index e760c2d343..adcef18cef 100644
--- a/src/frontends/lean/find_cmd.cpp
+++ b/src/frontends/lean/find_cmd.cpp
@@ -52,7 +52,7 @@ bool get_find_expensive(options const & opts) {
 }
 
 
-bool match_pattern(type_checker & tc, expr const & pattern, declaration const & d, unsigned max_steps, bool cheap) {
+bool match_pattern(old_type_checker & tc, expr const & pattern, declaration const & d, unsigned max_steps, bool cheap) {
     buffer<level> ls;
     unsigned num_ls = d.get_num_univ_params();
     for (unsigned i = 0; i < num_ls; i++)
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 2c1d1b22ee..cca3f4c167 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -147,7 +147,7 @@ struct inductive_cmd_fn {
 
     parser &            m_p;
     environment         m_env;
-    type_checker_ptr    m_tc;
+    old_type_checker_ptr    m_tc;
     name                m_namespace; // current namespace
     pos_info            m_pos; // current position for reporting errors
     bool                m_first; // true if parsing the first inductive type in a mutually recursive inductive decl.
diff --git a/src/frontends/lean/info_tactic.cpp b/src/frontends/lean/info_tactic.cpp
index 9a6f0b2047..d9b294bd9c 100644
--- a/src/frontends/lean/info_tactic.cpp
+++ b/src/frontends/lean/info_tactic.cpp
@@ -49,7 +49,7 @@ expr mk_info_tactic_expr() {
 
 void initialize_info_tactic() {
     register_tac(INFO_TAC_NAME,
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      return mk_info_tactic(fn, e);
                  });
 }
diff --git a/src/frontends/lean/parse_with_attributes_tactic.cpp b/src/frontends/lean/parse_with_attributes_tactic.cpp
index 8461d4ec02..20b6c4b51e 100644
--- a/src/frontends/lean/parse_with_attributes_tactic.cpp
+++ b/src/frontends/lean/parse_with_attributes_tactic.cpp
@@ -96,7 +96,7 @@ void initialize_with_attributes_tactic() {
     name with_attributes_tac_name{"tactic", "with_attributes_tac"};
     g_with_attributes_tac = new expr(Const(with_attributes_tac_name));
     register_tac(with_attributes_tac_name,
-                 [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
+                 [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
                      buffer<expr> args;
                      get_app_args(e, args);
                      if (args.size() != 3)
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 60f5df7098..3a8ad5ae45 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -82,7 +82,6 @@ static auto get_structure_info(environment const & env, name const & S)
 }
 
 struct structure_cmd_fn {
-    typedef std::unique_ptr<type_checker> type_checker_ptr;
     typedef std::vector<pair<name, name>> rename_vector;
     // field_map[i] contains the position of the \c i-th field of a parent structure into this one.
     typedef std::vector<unsigned>         field_map;
@@ -90,7 +89,7 @@ struct structure_cmd_fn {
 
     parser &                    m_p;
     environment                 m_env;
-    type_checker_ptr            m_tc;
+    old_type_checker_ptr        m_tc;
     name                        m_namespace;
     name                        m_name;
     pos_info                    m_name_pos;
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 7f2c6c0d00..bba69ee251 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -948,6 +948,7 @@ static optional<pair<expr, constraint_seq>> to_intro_when_K(inductive_env_ext::e
         });
     if (!ctx.is_def_eq(app_type, new_type, jst, cs))
         return none_ecs();
+    cs = constraint_seq();
     return some_ecs(*new_intro_app, cs);
 }
 
@@ -1009,6 +1010,7 @@ auto inductive_normalizer_extension::operator()(expr const & e, extension_contex
         unsigned num_args = elim_args.size() - major_idx - 1;
         r = mk_app(r, num_args, elim_args.data() + major_idx + 1);
     }
+    cs = constraint_seq();
     return some_ecs(r, cs);
 }
 
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 93b80c6d9d..534dc6922f 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -156,6 +156,7 @@ app_delayed_justification::app_delayed_justification(expr const & e, expr const
                                                      expr const & a_type):
     m_e(e), m_arg(arg), m_fn_type(f_type), m_arg_type(a_type) {}
 
+#if 0
 justification mk_app_justification(expr const & e, expr const & fn_type, expr const & arg, expr const & a_type) {
     auto pp_fn = [=](formatter const & fmt, substitution const & subst, bool as_error) {
         substitution s(subst);
@@ -163,6 +164,7 @@ justification mk_app_justification(expr const & e, expr const & fn_type, expr co
     };
     return mk_justification(e, pp_fn);
 }
+#endif
 
 justification app_delayed_justification::get() {
     if (!m_jst) {
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 07472a33c6..7cadef09fe 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -20,4 +20,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp
   attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp
   defeq_simplifier.cpp proof_irrel_expr_manager.cpp local_context.cpp metavar_context.cpp
-  legacy_type_context.cpp type_context.cpp)
+  legacy_type_context.cpp type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp)
diff --git a/src/library/blast/blast_tactic.cpp b/src/library/blast/blast_tactic.cpp
index b9c16ab58b..bf0c83b6da 100644
--- a/src/library/blast/blast_tactic.cpp
+++ b/src/library/blast/blast_tactic.cpp
@@ -38,7 +38,7 @@ tactic mk_blast_tactic(list<name> const & ls, list<name> const & ds) {
 
 void initialize_blast_tactic() {
     register_tac(name{"tactic", "blast"},
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                      buffer<expr> args;
                      get_app_args(e, args);
                      if (args.size() != 2)
diff --git a/src/library/class.cpp b/src/library/class.cpp
index fd959a554b..e06aa51bd2 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -231,7 +231,7 @@ bool is_class(environment const & env, name const & c) {
     return s.m_instances.contains(c);
 }
 
-type_checker_ptr mk_class_type_checker(environment const & env, bool conservative) {
+old_type_checker_ptr mk_class_type_checker(environment const & env, bool conservative) {
     auto pred = conservative ? mk_not_reducible_pred(env) : mk_irreducible_pred(env);
     class_state s = class_ext::get_state(env);
     return mk_type_checker(env, [=](name const & n) {
@@ -266,7 +266,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior
 
 static name * g_source = nullptr;
 
-static pair<name, name> get_source_target(environment const & env, type_checker & tc, name const & n) {
+static pair<name, name> get_source_target(environment const & env, old_type_checker & tc, name const & n) {
     buffer<expr> domain;
     declaration const & d = env.get(n);
     expr codomain      = to_telescope(tc, d.get_type(), domain);
@@ -289,7 +289,7 @@ static pair<name, name> get_source_target(environment const & env, type_checker
 }
 
 environment add_trans_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) {
-    type_checker_ptr  tc     = mk_type_checker(env);
+    old_type_checker_ptr  tc     = mk_type_checker(env);
     pair<name, name> src_tgt = get_source_target(env, *tc, n);
     class_state const & s = class_ext::get_state(env);
     tc_multigraph g    = s.m_mgraph;
@@ -363,7 +363,7 @@ static optional<name> constant_is_ext_class(environment const & env, expr const
     l_false:  \c type is not a class.
     l_undef:  procedure did not establish whether \c type is a class or not.
 */
-static lbool is_quick_ext_class(type_checker const & tc, expr const & type, name & result) {
+static lbool is_quick_ext_class(old_type_checker const & tc, expr const & type, name & result) {
     environment const & env = tc.env();
     expr const * it         = &type;
     while (true) {
@@ -407,7 +407,7 @@ static lbool is_quick_ext_class(type_checker const & tc, expr const & type, name
 }
 
 /** \brief Full/Expensive test for \c is_ext_class */
-static optional<name> is_full_ext_class(type_checker & tc, expr type) {
+static optional<name> is_full_ext_class(old_type_checker & tc, expr type) {
     type = tc.whnf(type).first;
     if (is_pi(type)) {
         return is_full_ext_class(tc, instantiate(binding_body(type), mk_local(mk_fresh_name(), binding_domain(type))));
@@ -420,7 +420,7 @@ static optional<name> is_full_ext_class(type_checker & tc, expr type) {
 }
 
 /** \brief Return true iff \c type is a class or Pi that produces a class. */
-optional<name> is_ext_class(type_checker & tc, expr const & type) {
+optional<name> is_ext_class(old_type_checker & tc, expr const & type) {
     name result;
     switch (is_quick_ext_class(tc, type, result)) {
     case l_true:  return optional<name>(result);
@@ -431,7 +431,7 @@ optional<name> is_ext_class(type_checker & tc, expr const & type) {
 }
 
 /** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
-list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name) {
+list<expr> get_local_instances(old_type_checker & tc, list<expr> const & ctx, name const & cls_name) {
     buffer<expr> buffer;
     for (auto const & l : ctx) {
         if (!is_local(l))
diff --git a/src/library/class.h b/src/library/class.h
index 5729b28b5b..9e72f2519f 100644
--- a/src/library/class.h
+++ b/src/library/class.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 namespace lean {
 /** \brief Create type checker that treats classes as opaque constants */
-type_checker_ptr mk_class_type_checker(environment const & env, bool conservative);
+old_type_checker_ptr mk_class_type_checker(environment const & env, bool conservative);
 /** \brief Add a new 'class' to the environment (if it is not already declared) */
 environment add_class(environment const & env, name const & n, name const & ns, bool persistent);
 /** \brief Add a new 'class instance' to the environment. */
@@ -34,7 +34,7 @@ void get_classes(environment const & env, buffer<name> & classes);
 name get_class_name(environment const & env, expr const & e);
 
 /** \brief Return true iff \c type is a class or Pi that produces a class. */
-optional<name> is_ext_class(type_checker & tc, expr const & type);
+optional<name> is_ext_class(old_type_checker & tc, expr const & type);
 
 /** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
 list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name);
diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp
index ebb9416280..13ded63b18 100644
--- a/src/library/class_instance_resolution.cpp
+++ b/src/library/class_instance_resolution.cpp
@@ -137,7 +137,7 @@ optional<expr> mk_class_instance(environment const & env, old_local_context cons
     return mk_class_instance(env, ctx.get_data(), type, nullptr);
 }
 
-optional<expr> mk_set_instance(type_checker & tc, options const & o, list<expr> const & ctx, expr const & type) {
+optional<expr> mk_set_instance(old_type_checker & tc, options const & o, list<expr> const & ctx, expr const & type) {
     level lvl        = sort_level(tc.ensure_type(type).first);
     expr is_set     = tc.whnf(mk_app(mk_constant(get_is_trunc_is_set_name(), {lvl}), type)).first;
     return mk_class_instance(tc.env(), o, ctx, is_set);
diff --git a/src/library/class_instance_resolution.h b/src/library/class_instance_resolution.h
index 834ce6e821..ed6233f5c2 100644
--- a/src/library/class_instance_resolution.h
+++ b/src/library/class_instance_resolution.h
@@ -39,7 +39,7 @@ pair<expr, constraint> mk_class_instance_elaborator(
 
 optional<expr> mk_class_instance(environment const & env, io_state const & ios, old_local_context const & ctx, expr const & type, bool use_local_instances);
 optional<expr> mk_class_instance(environment const & env, old_local_context const & ctx, expr const & type);
-optional<expr> mk_set_instance(type_checker & tc, options const & o, list<expr> const & ctx, expr const & type);
+optional<expr> mk_set_instance(old_type_checker & tc, options const & o, list<expr> const & ctx, expr const & type);
 optional<expr> mk_subsingleton_instance(environment const & env, options const & o,
                                         list<expr> const & ctx, expr const & type);
 
diff --git a/src/library/composition_manager.cpp b/src/library/composition_manager.cpp
index 63d99a87ee..746e7cb7df 100644
--- a/src/library/composition_manager.cpp
+++ b/src/library/composition_manager.cpp
@@ -7,11 +7,11 @@ Author: Leonardo de Moura
 #include <utility>
 #include <string>
 #include "util/sstream.h"
-#include "kernel/type_checker.h"
 #include "kernel/declaration.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/inductive/inductive.h"
+#include "library/old_type_checker.h"
 #include "library/replace_visitor.h"
 #include "library/reducible.h"
 #include "library/projection.h"
@@ -40,7 +40,7 @@ static environment update(environment const & env, composition_manager_ext const
 
 struct elim_proj_mk : public replace_visitor {
     environment const & m_env;
-    type_checker_ptr    m_tc;
+    old_type_checker_ptr    m_tc;
 
     virtual expr visit_binding(expr const & e) override {
         // stop at binders
@@ -96,7 +96,7 @@ static bool is_constructor_of_projections_decl(environment const & env, declarat
     return false;
 }
 
-pair<environment, name> compose(environment const & env, type_checker & tc, name const & g, name const & f, optional<name> const & gf) {
+pair<environment, name> compose(environment const & env, old_type_checker & tc, name const & g, name const & f, optional<name> const & gf) {
     composition_manager_ext ext = get_extension(env);
     if (name const * it = ext.m_cache.find(mk_pair(g, f)))
         return mk_pair(env, *it);
@@ -170,7 +170,7 @@ pair<environment, name> compose(environment const & env, type_checker & tc, name
 }
 
 pair<environment, name> compose(environment const & env, name const & g, name const & f, optional<name> const & gf) {
-    type_checker tc(env);
+    old_type_checker tc(env);
     return compose(env, tc, g, f, gf);
 }
 
diff --git a/src/library/composition_manager.h b/src/library/composition_manager.h
index 4ee4ed3a4b..628dd20b9a 100644
--- a/src/library/composition_manager.h
+++ b/src/library/composition_manager.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "kernel/type_checker.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 /** \brief Define the composition of g and f, if the environment already contains one created using \c compose, returns it.
@@ -13,7 +13,7 @@ namespace lean {
     If the environment already has a definition with this name, then adds the prefix _idx, where idx is a numeral.
     The result is a pair (new environment, new constant name).
 */
-pair<environment, name> compose(environment const & env, type_checker & tc, name const & g, name const & f, optional<name> const & gf = optional<name>());
+pair<environment, name> compose(environment const & env, old_type_checker & tc, name const & g, name const & f, optional<name> const & gf = optional<name>());
 pair<environment, name> compose(environment const & env, name const & g, name const & f, optional<name> const & gf = optional<name>());
 void initialize_composition_manager();
 void finalize_composition_manager();
diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp
index 52662afa31..f40bfbff61 100644
--- a/src/library/definitional/brec_on.cpp
+++ b/src/library/definitional/brec_on.cpp
@@ -44,7 +44,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
     if (is_inductive_predicate(env, n))
         return env;
     inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n);
-    type_checker tc(env);
+    old_type_checker tc(env);
     unsigned nparams       = std::get<1>(decls);
     declaration ind_decl   = env.get(n);
     declaration rec_decl   = env.get(inductive::get_elim_name(n));
@@ -167,7 +167,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
     if (is_inductive_predicate(env, n))
         return env;
     inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n);
-    type_checker tc(env);
+    old_type_checker tc(env);
     unsigned nparams       = std::get<1>(decls);
     declaration ind_decl   = env.get(n);
     declaration rec_decl   = env.get(inductive::get_elim_name(n));
diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index e8759556d4..3fb20018c4 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -299,7 +299,7 @@ void finalize_equations() {
 }
 
 class equation_compiler_fn {
-    type_checker &   m_tc;
+    old_type_checker &   m_tc;
     io_state const & m_ios;
     expr             m_meta;
     expr             m_meta_type;
@@ -1770,7 +1770,7 @@ class equation_compiler_fn {
 
 
 public:
-    equation_compiler_fn(type_checker & tc, io_state const & ios, expr const & meta, expr const & meta_type):
+    equation_compiler_fn(old_type_checker & tc, io_state const & ios, expr const & meta, expr const & meta_type):
         m_tc(tc), m_ios(ios), m_meta(meta), m_meta_type(meta_type) {
         get_app_args(m_meta, m_global_context);
     }
@@ -1793,7 +1793,7 @@ public:
     }
 };
 
-expr compile_equations(type_checker & tc, io_state const & ios, expr const & eqns,
+expr compile_equations(old_type_checker & tc, io_state const & ios, expr const & eqns,
                        expr const & meta, expr const & meta_type) {
     return equation_compiler_fn(tc, ios, meta, meta_type)(eqns);
 }
diff --git a/src/library/definitional/equations.h b/src/library/definitional/equations.h
index 1096cefa72..547e04f738 100644
--- a/src/library/definitional/equations.h
+++ b/src/library/definitional/equations.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-class type_checker;
+class old_type_checker;
 class io_state;
 
 bool is_equation(expr const & e);
@@ -41,7 +41,7 @@ expr update_equations(expr const & eqns, buffer<expr> const & new_eqs);
 expr mk_inaccessible(expr const & e);
 bool is_inaccessible(expr const & e);
 
-expr compile_equations(type_checker & tc, io_state const & ios, expr const & eqns,
+expr compile_equations(old_type_checker & tc, io_state const & ios, expr const & eqns,
                        expr const & meta, expr const & meta_type);
 
 /** \brief Return true if \c e is an auxiliary macro used to store the result of mutually recursive declarations.
diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp
index a4fcc7d669..ec1480d602 100644
--- a/src/library/definitional/no_confusion.cpp
+++ b/src/library/definitional/no_confusion.cpp
@@ -83,7 +83,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     cases_on       = mk_app(cases_on, nindices, args.data() + nparams);
     expr cases_on1 = mk_app(cases_on, v1);
     expr cases_on2 = mk_app(cases_on, v2);
-    type_checker tc(env);
+    old_type_checker tc(env);
     expr t1        = tc.infer(cases_on1).first;
     expr t2        = tc.infer(cases_on2).first;
     buffer<expr> outer_cases_on_args;
@@ -149,7 +149,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
     if (!env1)
         return env;
     environment new_env = *env1;
-    type_checker tc(new_env);
+    old_type_checker tc(new_env);
     bool impredicative                 = env.impredicative();
     inductive::inductive_decls decls   = *inductive::is_inductive_decl(new_env, n);
     unsigned nparams                   = std::get<1>(decls);
diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp
index 775a2fa9d1..729220a76f 100644
--- a/src/library/inductive_unifier_plugin.cpp
+++ b/src/library/inductive_unifier_plugin.cpp
@@ -12,15 +12,33 @@ Author: Leonardo de Moura
 #include "library/util.h"
 
 namespace lean {
+static optional<expr> is_elim_meta_app(old_type_checker & ctx, expr const & e) {
+    expr const & elim_fn   = get_app_fn(e);
+    if (!is_constant(elim_fn))
+        return none_expr();
+    unsigned major_idx = 0;
+    if (auto idx = inductive::get_elim_major_idx(ctx.env(), const_name(elim_fn)))
+        major_idx = *idx;
+    else
+        return none_expr();
+    buffer<expr> elim_args;
+    get_app_args(e, elim_args);
+    if (elim_args.size() < major_idx + 1)
+        return none_expr();
+    expr intro_app = ctx.whnf(elim_args[major_idx]).first;
+    return ctx.is_stuck(intro_app);
+}
+
 class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     /** \brief Return true iff the lhs or rhs of the constraint c is of the form (elim ... (?m ...) ...) */
-    bool is_elim_meta_cnstr(type_checker & tc, constraint const & c) const {
-        return is_eq_cnstr(c) && (inductive::is_elim_meta_app(tc, cnstr_lhs_expr(c)) ||
-                                  inductive::is_elim_meta_app(tc, cnstr_rhs_expr(c)));
+    bool is_elim_meta_cnstr(old_type_checker & tc, constraint const & c) const {
+        return false;
+        return is_eq_cnstr(c) && (is_elim_meta_app(tc, cnstr_lhs_expr(c)) ||
+                                  is_elim_meta_app(tc, cnstr_rhs_expr(c)));
     }
 
     /** \brief Return true iff \c e is of the form (?m ... (intro ...) ...) */
-    bool is_meta_intro_app(type_checker & tc, expr const & e) const {
+    bool is_meta_intro_app(old_type_checker & tc, expr const & e) const {
         if (!is_app(e) || !is_meta(e))
             return false;
         buffer<expr> args;
@@ -36,7 +54,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     }
 
     /** \brief Return true iff the lhs or rhs of the constraint c is of the form (?m ... (intro ...)) */
-    bool is_meta_intro_cnstr(type_checker & tc, constraint const & c) const {
+    bool is_meta_intro_cnstr(old_type_checker & tc, constraint const & c) const {
         return is_eq_cnstr(c) && (is_meta_intro_app(tc, cnstr_lhs_expr(c)) || is_meta_intro_app(tc, cnstr_rhs_expr(c)));
     }
 
@@ -45,7 +63,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
        and the major premise is of the form (?m ...), we create a case split where we try to assign (?m ...)
        to the different constructors of decl.
     */
-    lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, inductive::inductive_decl const & decl,
+    lazy_list<constraints> add_elim_meta_cnstrs(old_type_checker & tc, inductive::inductive_decl const & decl,
                                                 expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
                                                 constraint_seq cs) const {
         lean_assert(is_constant(elim));
@@ -90,8 +108,8 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
         return to_lazy(to_list(alts.begin(), alts.end()));
     }
 
-    lazy_list<constraints> process_elim_meta_core(type_checker & tc, expr const & lhs, expr const & rhs, justification const & j) const {
-        lean_assert(inductive::is_elim_meta_app(tc, lhs));
+    lazy_list<constraints> process_elim_meta_core(old_type_checker & tc, expr const & lhs, expr const & rhs, justification const & j) const {
+        lean_assert(is_elim_meta_app(tc, lhs));
         auto dcs = tc.is_def_eq_types(lhs, rhs, j);
         if (!dcs.first)
             return lazy_list<constraints>();
@@ -115,21 +133,21 @@ public:
        \brief Try to solve constraint of the form (elim ... (?m ...)) =?= t, by assigning (?m ...) to the introduction rules
        associated with the eliminator \c elim.
     */
-    virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c) const {
+    virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
         if (!is_eq_cnstr(c))
             return lazy_list<constraints>();
         expr const & lhs        = cnstr_lhs_expr(c);
         expr const & rhs        = cnstr_rhs_expr(c);
         justification const & j = c.get_justification();
-        if (inductive::is_elim_meta_app(tc, lhs))
+        if (is_elim_meta_app(tc, lhs))
             return process_elim_meta_core(tc, lhs, rhs, j);
-        else if (inductive::is_elim_meta_app(tc, rhs))
+        else if (is_elim_meta_app(tc, rhs))
             return process_elim_meta_core(tc, rhs, lhs, j);
         else
             return lazy_list<constraints>();
     }
 
-    virtual bool delay_constraint(type_checker & tc, constraint const & c) const {
+    virtual bool delay_constraint(old_type_checker & tc, constraint const & c) const {
         return is_elim_meta_cnstr(tc, c) || is_meta_intro_cnstr(tc, c);
     }
 };
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 67c674058b..bde98ac58a 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -54,8 +54,17 @@ Author: Leonardo de Moura
 #include "library/defeq_simp_lemmas.h"
 #include "library/defeq_simplifier.h"
 
+#include "library/old_converter.h"
+#include "library/old_default_converter.h"
+#include "library/old_type_checker.h"
+
+
 namespace lean {
 void initialize_library_module() {
+    initialize_old_converter();
+    initialize_old_default_converter();
+    initialize_old_type_checker();
+
     initialize_local_context();
     initialize_metavar_context();
     initialize_attribute_manager();
@@ -157,5 +166,9 @@ void finalize_library_module() {
     finalize_attribute_manager();
     finalize_metavar_context();
     finalize_local_context();
+
+    finalize_old_converter();
+    finalize_old_default_converter();
+    finalize_old_type_checker();
 }
 }
diff --git a/src/library/match.cpp b/src/library/match.cpp
index 922e614b69..a7706d5812 100644
--- a/src/library/match.cpp
+++ b/src/library/match.cpp
@@ -10,10 +10,10 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
-#include "kernel/type_checker.h"
 #include "library/locals.h"
 #include "library/match.h"
 #include "library/idx_metavar.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 class match_fn : public match_context {
diff --git a/src/library/match.h b/src/library/match.h
index bd94d1eeac..0992523a2e 100644
--- a/src/library/match.h
+++ b/src/library/match.h
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/environment.h"
 #include "library/idx_metavar.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 /** \brief Context for match_plugins. */
@@ -65,9 +66,9 @@ public:
 
 /** \brief Simple plugin that just puts terms in whnf and tries again */
 class whnf_match_plugin : public match_plugin {
-    type_checker & m_tc;
+    old_type_checker & m_tc;
 public:
-    whnf_match_plugin(type_checker & tc):m_tc(tc) {}
+    whnf_match_plugin(old_type_checker & tc):m_tc(tc) {}
     virtual bool on_failure(expr const & p, expr const & t, match_context & ctx) const;
 };
 
diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index a0635fea07..ba74cc91ad 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -8,10 +8,10 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/sstream.h"
 #include "kernel/for_each_fn.h"
-#include "kernel/type_checker.h"
 #include "library/module.h"
 #include "library/util.h"
 #include "library/fingerprint.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 struct noncomputable_ext : public environment_extension {
@@ -49,7 +49,7 @@ static void noncomputable_reader(deserializer & d, shared_environment & senv,
         });
 }
 
-static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, name const & n) {
+static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ext, name const & n) {
     if (ext.m_noncomputable.contains(n))
         return true;
     declaration const & d = tc.env().get(n);
@@ -57,7 +57,7 @@ static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, n
 }
 
 bool is_noncomputable(environment const & env, name const & n) {
-    type_checker tc(env);
+    old_type_checker tc(env);
     auto ext = get_extension(env);
     return is_noncomputable(tc, ext, n);
 }
@@ -80,7 +80,7 @@ optional<name> get_noncomputable_reason(environment const & env, name const & n)
     declaration const & d = env.get(n);
     if (!d.is_definition())
         return optional<name>();
-    type_checker tc(env);
+    old_type_checker tc(env);
     if (tc.is_prop(d.get_type()).first)
         return optional<name>(); // definition is a proposition, then do nothing
     expr const & v = d.get_value();
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 0fd21aa0bf..3187321724 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "util/interrupt.h"
 #include "util/fresh_name.h"
 #include "kernel/replace_fn.h"
-#include "kernel/type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/free_vars.h"
@@ -19,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 #include "library/kernel_serializer.h"
 #include "library/attribute_manager.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 /**
@@ -257,14 +257,14 @@ expr beta_eta_reduce(expr t) {
 }
 
 class normalize_fn {
-    type_checker   &                  m_tc;
+    old_type_checker   &                  m_tc;
     // Remark: the normalizer/type-checker m_tc has been provided by the "user".
     // It may be a constrained one (e.g., it may only unfold definitions marked as [reducible].
     // So, we should not use it for inferring types and/or checking whether an expression is
     // a proposition or not. Such checks may fail because of the restrictions on m_tc.
     // So, we use m_full_tc for this kind of operation. It is an unconstrained type checker.
     // See issue #801
-    type_checker                      m_full_tc;
+    old_type_checker                      m_full_tc;
     std::function<bool(expr const &)> m_pred;  // NOLINT
     bool                              m_save_cnstrs;
     constraint_seq                    m_cnstrs;
@@ -409,7 +409,7 @@ class normalize_fn {
     }
 
 public:
-    normalize_fn(type_checker & tc, bool save, bool eta, bool nested_prop = true):
+    normalize_fn(old_type_checker & tc, bool save, bool eta, bool nested_prop = true):
         m_tc(tc), m_full_tc(tc.env()),
         m_pred([](expr const &) { return true; }),
         m_save_cnstrs(save), m_use_eta(eta), m_eval_nested_prop(nested_prop) {
@@ -417,7 +417,7 @@ public:
             m_eval_nested_prop = true;
     }
 
-    normalize_fn(type_checker & tc, std::function<bool(expr const &)> const & fn, bool eta, bool nested_prop = true): // NOLINT
+    normalize_fn(old_type_checker & tc, std::function<bool(expr const &)> const & fn, bool eta, bool nested_prop = true): // NOLINT
         m_tc(tc), m_full_tc(tc.env()),
         m_pred(fn), m_save_cnstrs(true), m_use_eta(eta), m_eval_nested_prop(nested_prop) {
         if (!is_standard(env()))
@@ -451,17 +451,17 @@ expr normalize(environment const & env, level_param_names const & ls, expr const
     return normalize_fn(*tc, save_cnstrs, eta)(ls, e);
 }
 
-expr normalize(type_checker & tc, expr const & e, bool eta) {
+expr normalize(old_type_checker & tc, expr const & e, bool eta) {
     bool save_cnstrs = false;
     return normalize_fn(tc, save_cnstrs, eta)(e);
 }
 
-expr normalize(type_checker & tc, level_param_names const & ls, expr const & e, bool eta, bool eval_nested_prop) {
+expr normalize(old_type_checker & tc, level_param_names const & ls, expr const & e, bool eta, bool eval_nested_prop) {
     bool save_cnstrs = false;
     return normalize_fn(tc, save_cnstrs, eta, eval_nested_prop)(ls, e);
 }
 
-expr normalize(type_checker & tc, expr const & e, constraint_seq & cs, bool eta) {
+expr normalize(old_type_checker & tc, expr const & e, constraint_seq & cs, bool eta) {
     bool save_cnstrs = false;
     normalize_fn fn(tc, save_cnstrs, eta);
     expr r = fn(e);
@@ -469,7 +469,7 @@ expr normalize(type_checker & tc, expr const & e, constraint_seq & cs, bool eta)
     return r;
 }
 
-expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const &)> const & pred, // NOLINT
+expr normalize(old_type_checker & tc, expr const & e, std::function<bool(expr const &)> const & pred, // NOLINT
                constraint_seq & cs, bool eta) {
     normalize_fn fn(tc, pred, eta);
     expr r = fn(e);
diff --git a/src/library/normalize.h b/src/library/normalize.h
index 063befea4c..4346d7f2e5 100644
--- a/src/library/normalize.h
+++ b/src/library/normalize.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <functional>
-#include "kernel/type_checker.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 /** \brief Return the \c e normal form with respect to the environment \c env.
@@ -18,18 +18,18 @@ expr normalize(environment const & env, expr const & e, bool eta = false);
 expr normalize(environment const & env, level_param_names const & ls, expr const & e, bool eta = false);
 /** \brief Similar to <tt>expr normalize(environment const & env, expr const & e)</tt>, but
     uses the converter associated with \c tc. */
-expr normalize(type_checker & tc, expr const & e, bool eta = false);
-expr normalize(type_checker & tc, level_param_names const & ls, expr const & e, bool eta = false, bool eval_nested_prop = true);
+expr normalize(old_type_checker & tc, expr const & e, bool eta = false);
+expr normalize(old_type_checker & tc, level_param_names const & ls, expr const & e, bool eta = false, bool eval_nested_prop = true);
 /** \brief Return the \c e normal form with respect to \c tc, and store generated constraints
     into \c cs.
 */
-expr normalize(type_checker & tc, expr const & e, constraint_seq & cs, bool eta = false);
+expr normalize(old_type_checker & tc, expr const & e, constraint_seq & cs, bool eta = false);
 /** \brief Return the \c e normal form with respect to \c tc, and store generated constraints
     into \c cs.
 
     \remark A sub-expression is evaluated only if \c pred returns true.
 */
-expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const&)> const & pred, // NOLINT
+expr normalize(old_type_checker & tc, expr const & e, std::function<bool(expr const&)> const & pred, // NOLINT
                constraint_seq & cs, bool eta = false);
 
 /** \brief [unfold] hint instructs the normalizer (and simplifier) that
diff --git a/src/library/old_converter.cpp b/src/library/old_converter.cpp
new file mode 100644
index 0000000000..dcef97e5e5
--- /dev/null
+++ b/src/library/old_converter.cpp
@@ -0,0 +1,52 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/interrupt.h"
+#include "util/lbool.h"
+#include "kernel/expr_maps.h"
+#include "kernel/instantiate.h"
+#include "kernel/free_vars.h"
+#include "library/old_type_checker.h"
+#include "library/old_converter.h"
+#include "library/old_default_converter.h"
+
+
+namespace lean {
+static no_delayed_justification * g_no_delayed_jst = nullptr;
+
+pair<bool, constraint_seq> old_converter::is_def_eq(expr const & t, expr const & s, old_type_checker & c) {
+    return is_def_eq(t, s, c, *g_no_delayed_jst);
+}
+
+pair<expr, constraint_seq> old_converter::infer_type(old_type_checker & tc, expr const & e) { return tc.infer_type(e); }
+
+extension_context & old_converter::get_extension(old_type_checker & tc) { return tc.get_extension(); }
+
+/** \brief Do nothing old_converter */
+struct dummy_old_converter : public old_converter {
+    virtual pair<expr, constraint_seq> whnf(expr const & e, old_type_checker &) {
+        return mk_pair(e, constraint_seq());
+    }
+    virtual pair<bool, constraint_seq> is_def_eq(expr const &, expr const &, old_type_checker &, delayed_justification &) {
+        return mk_pair(true, constraint_seq());
+    }
+    virtual bool is_opaque(declaration const &) const { return false; }
+    virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
+    virtual optional<expr> is_stuck(expr const &, old_type_checker &) { return none_expr(); }
+};
+
+std::unique_ptr<old_converter> mk_dummy_old_converter() {
+    return std::unique_ptr<old_converter>(new dummy_old_converter());
+}
+
+void initialize_old_converter() {
+    g_no_delayed_jst      = new no_delayed_justification();
+}
+
+void finalize_old_converter() {
+    delete g_no_delayed_jst;
+}
+}
diff --git a/src/library/old_converter.h b/src/library/old_converter.h
new file mode 100644
index 0000000000..cd73e09f5f
--- /dev/null
+++ b/src/library/old_converter.h
@@ -0,0 +1,43 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <functional>
+#include "kernel/environment.h"
+
+namespace lean {
+class old_type_checker;
+
+class old_converter {
+protected:
+    pair<expr, constraint_seq> infer_type(old_type_checker & tc, expr const & e);
+    extension_context & get_extension(old_type_checker & tc);
+public:
+    virtual ~old_converter() {}
+    virtual bool is_opaque(declaration const & d) const = 0;
+    virtual optional<declaration> is_delta(expr const & e) const = 0;
+
+    virtual optional<expr> is_stuck(expr const & e, old_type_checker & c) = 0;
+    virtual pair<expr, constraint_seq> whnf(expr const & e, old_type_checker & c) = 0;
+    virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, old_type_checker & c, delayed_justification & j) = 0;
+
+    pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, old_type_checker & c);
+};
+
+/** \brief Old_Converter that allows us to specify constants that should be considered opaque */
+template<typename Old_Converter>
+class hint_old_converter : public Old_Converter {
+    name_predicate m_pred;
+public:
+    hint_old_converter(environment const & env, name_predicate const & p):Old_Converter(env), m_pred(p) {}
+    virtual bool is_opaque(declaration const & d) const { return m_pred(d.get_name()) || Old_Converter::is_opaque(d); }
+};
+
+std::unique_ptr<old_converter> mk_dummy_old_converter();
+
+void initialize_old_converter();
+void finalize_old_converter();
+}
diff --git a/src/library/old_default_converter.cpp b/src/library/old_default_converter.cpp
new file mode 100644
index 0000000000..93a9fddb93
--- /dev/null
+++ b/src/library/old_default_converter.cpp
@@ -0,0 +1,665 @@
+/*
+Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/interrupt.h"
+#include "util/flet.h"
+#include "util/fresh_name.h"
+#include "kernel/instantiate.h"
+#include "kernel/free_vars.h"
+#include "kernel/metavar.h"
+#include "kernel/error_msgs.h"
+#include "library/old_type_checker.h"
+#include "library/old_default_converter.h"
+
+namespace lean {
+static expr * g_dont_care = nullptr;
+
+old_default_converter::old_default_converter(environment const & env, bool memoize):
+    m_env(env), m_memoize(memoize) {
+    m_tc  = nullptr;
+    m_jst = nullptr;
+}
+
+constraint old_default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+    return ::lean::mk_eq_cnstr(lhs, rhs, j);
+}
+
+optional<expr> old_default_converter::expand_macro(expr const & m) {
+    lean_assert(is_macro(m));
+    return macro_def(m).expand(m, get_extension(*m_tc));
+}
+
+/** \brief Apply normalizer extensions to \c e. */
+optional<pair<expr, constraint_seq>> old_default_converter::norm_ext(expr const & e) {
+    return m_env.norm_ext()(e, get_extension(*m_tc));
+}
+
+optional<expr> old_default_converter::d_norm_ext(expr const & e, constraint_seq & cs) {
+    if (auto r = norm_ext(e)) {
+        cs += r->second;
+        return some_expr(r->first);
+    } else {
+        return none_expr();
+    }
+}
+
+/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
+bool old_default_converter::is_stuck(expr const & e) {
+    return static_cast<bool>(m_env.norm_ext().is_stuck(e, get_extension(*m_tc)));
+}
+
+optional<expr> old_default_converter::is_stuck(expr const & e, old_type_checker & c) {
+    if (is_meta(e)) {
+        return some_expr(e);
+    } else {
+        return m_env.norm_ext().is_stuck(e, get_extension(c));
+    }
+}
+
+/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
+expr old_default_converter::whnf_core(expr const & e) {
+    check_system("whnf");
+
+    // handle easy cases
+    switch (e.kind()) {
+    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
+        return e;
+    case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
+        break;
+    }
+
+    // check cache
+    if (m_memoize) {
+        auto it = m_whnf_core_cache.find(e);
+        if (it != m_whnf_core_cache.end())
+            return it->second;
+    }
+
+    // do the actual work
+    expr r;
+    switch (e.kind()) {
+    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
+        lean_unreachable(); // LCOV_EXCL_LINE
+    case expr_kind::Macro:
+        if (auto m = expand_macro(e))
+            r = whnf_core(*m);
+        else
+            r = e;
+        break;
+    case expr_kind::App: {
+        buffer<expr> args;
+        expr f0 = get_app_rev_args(e, args);
+        expr f = whnf_core(f0);
+        if (is_lambda(f)) {
+            unsigned m = 1;
+            unsigned num_args = args.size();
+            while (is_lambda(binding_body(f)) && m < num_args) {
+                f = binding_body(f);
+                m++;
+            }
+            lean_assert(m <= num_args);
+            r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()));
+        } else {
+            r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()));
+        }
+        break;
+    }
+    case expr_kind::Let:
+        r = whnf_core(instantiate(let_body(e), let_value(e)));
+        break;
+    }
+
+    if (m_memoize)
+        m_whnf_core_cache.insert(mk_pair(e, r));
+    return r;
+}
+
+bool old_default_converter::is_opaque(declaration const &) const {
+    return false;
+}
+
+/** \brief Expand \c e if it is non-opaque constant with height >= h */
+expr old_default_converter::unfold_name_core(expr e, unsigned h) {
+    if (is_constant(e)) {
+        if (auto d = m_env.find(const_name(e))) {
+            if (d->is_definition() && !is_opaque(*d) && d->get_height() >= h &&
+                length(const_levels(e)) == d->get_num_univ_params())
+                return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h);
+        }
+    }
+    return e;
+}
+
+/**
+   \brief Expand constants and application where the function is a constant.
+
+   The unfolding is only performend if the constant corresponds to
+   a non-opaque definition with height >= h.
+*/
+expr old_default_converter::unfold_names(expr const & e, unsigned h) {
+    if (is_app(e)) {
+        expr f0 = get_app_fn(e);
+        expr f  = unfold_name_core(f0, h);
+        if (is_eqp(f, f0)) {
+            return e;
+        } else {
+            buffer<expr> args;
+            get_app_rev_args(e, args);
+            return mk_rev_app(f, args);
+        }
+    } else {
+        return unfold_name_core(e, h);
+    }
+}
+
+/**
+   \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
+   to be expanded.
+*/
+optional<declaration> old_default_converter::is_delta(expr const & e) const {
+    expr const & f = get_app_fn(e);
+    if (is_constant(f)) {
+        if (auto d = m_env.find(const_name(f)))
+            if (d->is_definition() && !is_opaque(*d))
+                return d;
+    }
+    return none_declaration();
+}
+
+/**
+   \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
+   height greater than or equal to \c h.
+
+   This method is based on <tt>whnf_core(expr const &)</tt> and \c unfold_names.
+
+   \remark This method does not use normalization extensions attached in the environment.
+*/
+expr old_default_converter::whnf_core(expr e, unsigned h) {
+    while (true) {
+        expr new_e = unfold_names(whnf_core(e), h);
+        if (is_eqp(e, new_e))
+            return e;
+        e = new_e;
+    }
+}
+
+/** \brief Put expression \c t in weak head normal form */
+pair<expr, constraint_seq> old_default_converter::whnf(expr const & e_prime) {
+    // Do not cache easy cases
+    switch (e_prime.kind()) {
+    case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi:
+        return to_ecs(e_prime);
+    case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
+    case expr_kind::Constant: case expr_kind::Let:
+        break;
+    }
+
+    expr e = e_prime;
+    // check cache
+    if (m_memoize) {
+        auto it = m_whnf_cache.find(e);
+        if (it != m_whnf_cache.end())
+            return it->second;
+    }
+
+    expr t = e;
+    constraint_seq cs;
+    while (true) {
+        expr t1 = whnf_core(t, 0);
+        if (auto new_t = d_norm_ext(t1, cs)) {
+            t  = *new_t;
+        } else {
+            auto r = mk_pair(t1, cs);
+            if (m_memoize)
+                m_whnf_cache.insert(mk_pair(e, r));
+            return r;
+        }
+    }
+}
+
+expr old_default_converter::whnf(expr const & e_prime, constraint_seq & cs) {
+    auto r = whnf(e_prime);
+    cs += r.second;
+    return r.first;
+}
+
+/**
+   \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s.
+
+        t and s are definitionally equal
+           iff
+        domain(t) is definitionally equal to domain(s)
+        and
+        body(t) is definitionally equal to body(s)
+*/
+bool old_default_converter::is_def_eq_binding(expr t, expr s, constraint_seq & cs) {
+    lean_assert(t.kind() == s.kind());
+    lean_assert(is_binding(t));
+    expr_kind k = t.kind();
+    buffer<expr> subst;
+    do {
+        optional<expr> var_s_type;
+        if (binding_domain(t) != binding_domain(s)) {
+            var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
+            expr var_t_type = instantiate_rev(binding_domain(t), subst.size(), subst.data());
+            if (!is_def_eq(var_t_type, *var_s_type, cs))
+                return false;
+        }
+        if (!closed(binding_body(t)) || !closed(binding_body(s))) {
+            // local is used inside t or s
+            if (!var_s_type)
+                var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
+            subst.push_back(mk_local(mk_fresh_name(), binding_name(s), *var_s_type, binding_info(s)));
+        } else {
+            subst.push_back(*g_dont_care); // don't care
+        }
+        t = binding_body(t);
+        s = binding_body(s);
+    } while (t.kind() == k && s.kind() == k);
+    return is_def_eq(instantiate_rev(t, subst.size(), subst.data()),
+                     instantiate_rev(s, subst.size(), subst.data()), cs);
+}
+
+bool old_default_converter::is_def_eq(level const & l1, level const & l2, constraint_seq & cs) {
+    if (is_equivalent(l1, l2)) {
+        return true;
+    } else if (has_meta(l1) || has_meta(l2)) {
+        cs += constraint_seq(mk_level_eq_cnstr(l1, l2, m_jst->get()));
+        return true;
+    } else {
+        return false;
+    }
+}
+
+bool old_default_converter::is_def_eq(levels const & ls1, levels const & ls2, constraint_seq & cs) {
+    if (is_nil(ls1) && is_nil(ls2)) {
+        return true;
+    } else if (!is_nil(ls1) && !is_nil(ls2)) {
+        return
+            is_def_eq(head(ls1), head(ls2), cs) &&
+            is_def_eq(tail(ls1), tail(ls2), cs);
+    } else {
+        return false;
+    }
+}
+
+/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
+lbool old_default_converter::quick_is_def_eq(expr const & t, expr const & s, constraint_seq & cs, bool use_hash) {
+    if (m_eqv_manager.is_equiv(t, s, use_hash))
+        return l_true;
+    if (is_meta(t) || is_meta(s)) {
+        // if t or s is a metavariable (or the application of a metavariable), then add constraint
+        cs += constraint_seq(mk_eq_cnstr(t, s, m_jst->get()));
+        return l_true;
+    }
+    if (t.kind() == s.kind()) {
+        switch (t.kind()) {
+        case expr_kind::Lambda: case expr_kind::Pi:
+            return to_lbool(is_def_eq_binding(t, s, cs));
+        case expr_kind::Sort:
+            return to_lbool(is_def_eq(sort_level(t), sort_level(s), cs));
+        case expr_kind::Meta:
+            lean_unreachable(); // LCOV_EXCL_LINE
+        case expr_kind::Var:      case expr_kind::Local: case expr_kind::App:
+        case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
+            // We do not handle these cases in this method.
+            break;
+        }
+    }
+    return l_undef; // This is not an "easy case"
+}
+
+/**
+   \brief Return true if arguments of \c t are definitionally equal to arguments of \c s.
+   This method is used to implement an optimization in the method \c is_def_eq.
+*/
+bool old_default_converter::is_def_eq_args(expr t, expr s, constraint_seq & cs) {
+    while (is_app(t) && is_app(s)) {
+        if (!is_def_eq(app_arg(t), app_arg(s), cs))
+            return false;
+        t = app_fn(t);
+        s = app_fn(s);
+    }
+    return !is_app(t) && !is_app(s);
+}
+
+/** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
+bool old_default_converter::try_eta_expansion_core(expr const & t, expr const & s, constraint_seq & cs) {
+    if (is_lambda(t) && !is_lambda(s)) {
+        auto tcs    = infer_type(s);
+        auto wcs    = whnf(tcs.first);
+        expr s_type = wcs.first;
+        constraint_seq aux_cs;
+        if (is_pi(s_type)) {
+            // do nothing ... s_type is already a Pi
+        } else if (auto m = m_tc->is_stuck(s_type)) {
+            expr r              = mk_pi_for(*m);
+            justification j     = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) {
+                    return pp_function_expected(fmt, substitution(subst).instantiate(s));
+                });
+            aux_cs += mk_eq_cnstr(s_type, r, j);
+            s_type  = r;
+        } else {
+            return false;
+        }
+        expr new_s  = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type));
+        auto dcs    = is_def_eq(t, new_s);
+        if (!dcs.first) {
+            return false;
+        }
+        cs += dcs.second + wcs.second + tcs.second + aux_cs;
+        return true;
+    } else {
+        return false;
+    }
+}
+
+/** \brief Return true iff \c t and \c s are definitionally equal.
+
+    \remark Store in \c cs any generated constraints.
+*/
+bool old_default_converter::is_def_eq(expr const & t, expr const & s, constraint_seq & cs) {
+    auto bcs = is_def_eq(t, s);
+    if (bcs.first) {
+        cs += bcs.second;
+        return true;
+    } else {
+        return false;
+    }
+}
+
+/** \brief Return true if \c t and \c s are definitionally equal because they are applications of the form
+    <tt>(f a_1 ... a_n)</tt> <tt>(g b_1 ... b_n)</tt>, and \c f and \c g are definitionally equal, and
+    \c a_i and \c b_i are also definitionally equal for every 1 <= i <= n.
+    Return false otherwise.
+
+    \remark Store in \c cs any generated constraints
+*/
+bool old_default_converter::is_def_eq_app(expr const & t, expr const & s, constraint_seq & cs) {
+    if (is_app(t) && is_app(s)) {
+        buffer<expr> t_args;
+        buffer<expr> s_args;
+        expr t_fn = get_app_args(t, t_args);
+        expr s_fn = get_app_args(s, s_args);
+        constraint_seq cs_prime = cs;
+        if (is_def_eq(t_fn, s_fn, cs_prime) && t_args.size() == s_args.size()) {
+            unsigned i = 0;
+            for (; i < t_args.size(); i++) {
+                if (!is_def_eq(t_args[i], s_args[i], cs_prime))
+                    break;
+            }
+            if (i == t_args.size()) {
+                cs = cs_prime;
+                return true;
+            }
+        }
+    }
+    return false;
+}
+
+/** \brief remark: is_prop returns true only if \c e is reducible to Prop.
+    If \c e contains metavariables, then reduction can get stuck, and is_prop will return false.
+*/
+pair<bool, constraint_seq> old_default_converter::is_prop(expr const & e) {
+    auto tcs = infer_type(e);
+    auto wcs = whnf(tcs.first);
+    if (wcs.first == mk_Prop())
+        return to_bcs(true, wcs.second + tcs.second);
+    else
+        return to_bcs(false);
+}
+
+/** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant.
+    Return false otherwise.
+
+    \remark Store in \c cs any generated constraints.
+*/
+bool old_default_converter::is_def_eq_proof_irrel(expr const & t, expr const & s, constraint_seq & cs) {
+    if (!m_env.prop_proof_irrel())
+        return false;
+    // Proof irrelevance support for Prop (aka Type.{0})
+    auto tcs    = infer_type(t);
+    auto scs    = infer_type(s);
+    expr t_type = tcs.first;
+    expr s_type = scs.first;
+    auto pcs    = is_prop(t_type);
+    if (pcs.first) {
+        auto dcs = is_def_eq(t_type, s_type);
+        if (dcs.first) {
+            cs += dcs.second + scs.second + pcs.second + tcs.second;
+            return true;
+        }
+    } else {
+        // If we can't stablish whether t_type is Prop, we try s_type.
+        pcs = is_prop(s_type);
+        if (pcs.first) {
+            auto dcs = is_def_eq(t_type, s_type);
+            if (dcs.first) {
+                cs += dcs.second + scs.second + pcs.second + tcs.second;
+                return true;
+            }
+        }
+        // This procedure will miss the case where s_type and t_type cannot be reduced to Prop
+        // because they contain metavariables.
+    }
+    return false;
+}
+
+bool old_default_converter::failed_before(expr const & t, expr const & s) const {
+    if (t.hash() < s.hash()) {
+        return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end();
+    } else if (t.hash() > s.hash()) {
+        return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
+    } else {
+        return
+            m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end() ||
+            m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
+    }
+}
+
+void old_default_converter::cache_failure(expr const & t, expr const & s) {
+    if (t.hash() <= s.hash())
+        m_failure_cache.insert(mk_pair(t, s));
+    else
+        m_failure_cache.insert(mk_pair(s, t));
+}
+
+/**
+   \brief Perform one lazy delta-reduction step.
+   Return
+   - l_true if t_n and s_n are definitionally equal.
+   - l_false if they are not definitionally equal.
+   - l_undef it the step did not manage to establish whether they are definitionally equal or not.
+
+   \remark t_n, s_n and cs are updated.
+*/
+auto old_default_converter::lazy_delta_reduction_step(expr & t_n, expr & s_n, constraint_seq & cs) -> reduction_status {
+    auto d_t = is_delta(t_n);
+    auto d_s = is_delta(s_n);
+    if (!d_t && !d_s) {
+        return reduction_status::DefUnknown;
+    } else if (d_t && !d_s) {
+        t_n = whnf_core(unfold_names(t_n, 0));
+    } else if (!d_t && d_s) {
+        s_n = whnf_core(unfold_names(s_n, 0));
+    } else if (!d_t->is_theorem() && d_s->is_theorem()) {
+        t_n = whnf_core(unfold_names(t_n, d_t->get_height()));
+    } else if (!d_s->is_theorem() && d_t->is_theorem()) {
+        s_n = whnf_core(unfold_names(s_n, d_s->get_height()));
+    } else if (!d_t->is_theorem() && d_t->get_height() > d_s->get_height()) {
+        t_n = whnf_core(unfold_names(t_n, d_s->get_height() + 1));
+    } else if (!d_s->is_theorem() && d_t->get_height() < d_s->get_height()) {
+        s_n = whnf_core(unfold_names(s_n, d_t->get_height() + 1));
+    } else {
+        if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) {
+            // If t_n and s_n are both applications of the same (non-opaque) definition,
+            if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
+                // We let the unifier deal with cases such as
+                // (f ...) =?= (f ...)
+                // when t_n or s_n contains metavariables
+                return reduction_status::DefUnknown;
+            } else {
+                // Optimization:
+                // We try to check if their arguments are definitionally equal.
+                // If they are, then t_n and s_n must be definitionally equal, and we can
+                // skip the delta-reduction step.
+                // If the flag use_conv_opt() is not true, then we skip this optimization
+                constraint_seq tmp_cs;
+                if (!is_opaque(*d_t) && d_t->use_conv_opt() && !failed_before(t_n, s_n)) {
+                    if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n)), tmp_cs) &&
+                        is_def_eq_args(t_n, s_n, tmp_cs)) {
+                        cs += tmp_cs;
+                        return reduction_status::DefEqual;
+                    } else {
+                        cache_failure(t_n, s_n);
+                    }
+                }
+            }
+        }
+        t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1));
+        s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1));
+    }
+    switch (quick_is_def_eq(t_n, s_n, cs)) {
+    case l_true:  return reduction_status::DefEqual;
+    case l_false: return reduction_status::DefDiff;
+    case l_undef: return reduction_status::Continue;
+    }
+    lean_unreachable();
+}
+
+lbool old_default_converter::lazy_delta_reduction(expr & t_n, expr & s_n, constraint_seq & cs) {
+    while (true) {
+        switch (lazy_delta_reduction_step(t_n, s_n, cs)) {
+        case reduction_status::Continue:   break;
+        case reduction_status::DefUnknown: return l_undef;
+        case reduction_status::DefEqual:   return l_true;
+        case reduction_status::DefDiff:    return l_false;
+        }
+    }
+}
+
+auto old_default_converter::ext_reduction_step(expr & t_n, expr & s_n, constraint_seq & cs) -> reduction_status {
+    auto new_t_n = d_norm_ext(t_n, cs);
+    auto new_s_n = d_norm_ext(s_n, cs);
+    if (!new_t_n && !new_s_n)
+        return reduction_status::DefUnknown;
+    if (new_t_n)
+        t_n = whnf_core(*new_t_n);
+    if (new_s_n)
+        s_n = whnf_core(*new_s_n);
+    switch (quick_is_def_eq(t_n, s_n, cs)) {
+    case l_true:  return reduction_status::DefEqual;
+    case l_false: return reduction_status::DefDiff;
+    case l_undef: return reduction_status::Continue;
+    }
+    lean_unreachable();
+}
+
+// Apply lazy delta-reduction and then normalizer extensions
+lbool old_default_converter::reduce_def_eq(expr & t_n, expr & s_n, constraint_seq & cs) {
+    while (true) {
+        // first, keep applying lazy delta-reduction while applicable
+        lbool r = lazy_delta_reduction(t_n, s_n, cs);
+        if (r != l_undef) return r;
+
+        // try normalizer extensions
+        switch (ext_reduction_step(t_n, s_n, cs)) {
+        case reduction_status::Continue:   break;
+        case reduction_status::DefUnknown: return l_undef;
+        case reduction_status::DefEqual:   return l_true;
+        case reduction_status::DefDiff:    return l_false;
+        }
+    }
+}
+
+bool old_default_converter::postpone_is_def_eq(expr const & t, expr const & s) {
+    if (has_expr_metavar(t) || has_expr_metavar(s)) {
+        optional<declaration> d_t = is_delta(t);
+        optional<declaration> d_s = is_delta(s);
+        if (d_t && d_s && is_eqp(*d_t, *d_s))
+            return true;
+        else if (is_stuck(t) && is_stuck(s))
+            return true;
+    }
+    return false;
+}
+
+pair<bool, constraint_seq> old_default_converter::is_def_eq_core(expr const & t, expr const & s) {
+    check_system("is_definitionally_equal");
+    constraint_seq cs;
+    bool use_hash = true;
+    lbool r = quick_is_def_eq(t, s, cs, use_hash);
+    if (r != l_undef) return to_bcs(r == l_true, cs);
+
+    // apply whnf (without using delta-reduction or normalizer extensions)
+    expr t_n = whnf_core(t);
+    expr s_n = whnf_core(s);
+
+    if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) {
+        r = quick_is_def_eq(t_n, s_n, cs);
+        if (r != l_undef) return to_bcs(r == l_true, cs);
+    }
+
+    r = reduce_def_eq(t_n, s_n, cs);
+    if (r != l_undef) return to_bcs(r == l_true, cs);
+
+    if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n) &&
+        is_def_eq(const_levels(t_n), const_levels(s_n), cs))
+        return to_bcs(true, cs);
+
+    if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
+        return to_bcs(true, cs);
+
+    bool postpone = postpone_is_def_eq(t_n, s_n);
+
+    // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
+    if (!postpone && is_def_eq_app(t_n, s_n, cs))
+        return to_bcs(true, cs);
+
+    if (try_eta_expansion(t_n, s_n, cs))
+        return to_bcs(true, cs);
+
+    constraint_seq pi_cs;
+    if (is_def_eq_proof_irrel(t, s, pi_cs))
+        return to_bcs(true, pi_cs);
+
+    if (is_stuck(t_n) || is_stuck(s_n) || postpone) {
+        cs += constraint_seq(mk_eq_cnstr(t_n, s_n, m_jst->get()));
+        return to_bcs(true, cs);
+    }
+
+    return to_bcs(false);
+}
+
+pair<bool, constraint_seq> old_default_converter::is_def_eq(expr const & t, expr const & s) {
+    auto r = is_def_eq_core(t, s);
+    if (r.first && !r.second)
+        m_eqv_manager.add_equiv(t, s);
+    return r;
+}
+
+/** Return true iff t is definitionally equal to s. */
+pair<bool, constraint_seq> old_default_converter::is_def_eq(expr const & t, expr const & s, old_type_checker & c, delayed_justification & jst) {
+    flet<old_type_checker*>          set_tc(m_tc, &c);
+    flet<delayed_justification*> set_js(m_jst, &jst);
+    return is_def_eq(t, s);
+}
+
+pair<expr, constraint_seq> old_default_converter::whnf(expr const & e, old_type_checker & c) {
+    flet<old_type_checker*>          set_tc(m_tc, &c);
+    return whnf(e);
+}
+
+void initialize_old_default_converter() {
+    g_dont_care = new expr(Const("dontcare"));
+}
+
+void finalize_old_default_converter() {
+    delete g_dont_care;
+}
+}
diff --git a/src/library/old_default_converter.h b/src/library/old_default_converter.h
new file mode 100644
index 0000000000..158774526e
--- /dev/null
+++ b/src/library/old_default_converter.h
@@ -0,0 +1,100 @@
+/*
+Copyright (c) 2014-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 <unordered_set>
+#include "util/lbool.h"
+#include "kernel/justification.h"
+#include "kernel/environment.h"
+#include "kernel/expr_maps.h"
+#include "kernel/equiv_manager.h"
+#include "kernel/expr_pair.h"
+#include "library/old_converter.h"
+
+namespace lean {
+/** \brief Converter used in the kernel */
+class old_default_converter : public old_converter {
+protected:
+    typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
+    environment                                 m_env;
+    bool                                        m_memoize;
+    expr_struct_map<expr>                       m_whnf_core_cache;
+    expr_struct_map<pair<expr, constraint_seq>> m_whnf_cache;
+    equiv_manager                               m_eqv_manager;
+    expr_pair_set                               m_failure_cache;
+
+    // The two auxiliary fields are set when the public methods whnf and is_def_eq are invoked.
+    // The goal is to avoid to keep carrying them around.
+    old_type_checker *                          m_tc;
+    delayed_justification *                     m_jst;
+
+    virtual bool is_stuck(expr const & e);
+    virtual optional<pair<expr, constraint_seq>> norm_ext(expr const & e);
+
+    pair<expr, constraint_seq> infer_type(expr const & e) { return old_converter::infer_type(*m_tc, e); }
+    constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+    optional<expr> expand_macro(expr const & m);
+    optional<expr> d_norm_ext(expr const & e, constraint_seq & cs);
+    expr whnf_core(expr const & e);
+    expr unfold_name_core(expr e, unsigned w);
+    expr unfold_names(expr const & e, unsigned w);
+    expr whnf_core(expr e, unsigned w);
+
+    expr whnf(expr const & e_prime, constraint_seq & cs);
+
+    pair<bool, constraint_seq> to_bcs(bool b) { return mk_pair(b, constraint_seq()); }
+    pair<bool, constraint_seq> to_bcs(bool b, constraint const & c) { return mk_pair(b, constraint_seq(c)); }
+    pair<bool, constraint_seq> to_bcs(bool b, constraint_seq const & cs) { return mk_pair(b, cs); }
+
+    bool is_def_eq_binding(expr t, expr s, constraint_seq & cs);
+    bool is_def_eq(level const & l1, level const & l2, constraint_seq & cs);
+    bool is_def_eq(levels const & ls1, levels const & ls2, constraint_seq & cs);
+
+    static pair<lbool, constraint_seq> to_lbcs(lbool l) { return mk_pair(l, constraint_seq()); }
+    static pair<lbool, constraint_seq> to_lbcs(lbool l, constraint const & c) { return mk_pair(l, constraint_seq(c)); }
+    static pair<lbool, constraint_seq> to_lbcs(pair<bool, constraint_seq> const & bcs) {
+        return mk_pair(to_lbool(bcs.first), bcs.second);
+    }
+
+    lbool quick_is_def_eq(expr const & t, expr const & s, constraint_seq & cs, bool use_hash = false);
+    bool is_def_eq_args(expr t, expr s, constraint_seq & cs);
+    bool try_eta_expansion_core(expr const & t, expr const & s, constraint_seq & cs);
+    bool try_eta_expansion(expr const & t, expr const & s, constraint_seq & cs) {
+        return try_eta_expansion_core(t, s, cs) || try_eta_expansion_core(s, t, cs);
+    }
+    bool is_def_eq(expr const & t, expr const & s, constraint_seq & cs);
+    bool is_def_eq_app(expr const & t, expr const & s, constraint_seq & cs);
+    bool is_def_eq_proof_irrel(expr const & t, expr const & s, constraint_seq & cs);
+
+    bool failed_before(expr const & t, expr const & s) const;
+    void cache_failure(expr const & t, expr const & s);
+
+    pair<bool, constraint_seq> is_prop(expr const & e);
+    pair<expr, constraint_seq> whnf(expr const & e_prime);
+    pair<bool, constraint_seq> is_def_eq_core(expr const & t, expr const & s);
+    pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);
+
+    enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
+    reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n, constraint_seq & cs);
+    lbool lazy_delta_reduction(expr & t_n, expr & s_n, constraint_seq & cs);
+    reduction_status ext_reduction_step(expr & t_n, expr & s_n, constraint_seq & cs);
+    virtual lbool reduce_def_eq(expr & t_n, expr & s_n, constraint_seq & cs);
+
+    virtual bool postpone_is_def_eq(expr const & t, expr const & s);
+public:
+    old_default_converter(environment const & env, bool memoize = true);
+
+    virtual optional<declaration> is_delta(expr const & e) const;
+    virtual bool is_opaque(declaration const & d) const;
+
+    virtual optional<expr> is_stuck(expr const & e, old_type_checker & c);
+    virtual pair<expr, constraint_seq> whnf(expr const & e_prime, old_type_checker & c);
+    virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, old_type_checker & c, delayed_justification & jst);
+};
+
+void initialize_old_default_converter();
+void finalize_old_default_converter();
+}
diff --git a/src/library/old_type_checker.cpp b/src/library/old_type_checker.cpp
new file mode 100644
index 0000000000..f988567013
--- /dev/null
+++ b/src/library/old_type_checker.cpp
@@ -0,0 +1,466 @@
+/*
+Copyright (c) 2013-14 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <utility>
+#include <vector>
+#include "util/interrupt.h"
+#include "util/lbool.h"
+#include "util/flet.h"
+#include "util/sstream.h"
+#include "util/scoped_map.h"
+#include "util/fresh_name.h"
+#include "kernel/expr_maps.h"
+#include "kernel/instantiate.h"
+#include "kernel/free_vars.h"
+#include "kernel/metavar.h"
+#include "kernel/error_msgs.h"
+#include "kernel/kernel_exception.h"
+#include "kernel/abstract.h"
+#include "kernel/replace_fn.h"
+#include "library/old_default_converter.h"
+#include "library/old_type_checker.h"
+
+namespace lean {
+#if 0
+expr replace_range(expr const & type, expr const & new_range) {
+    if (is_pi(type))
+        return update_binding(type, binding_domain(type), replace_range(binding_body(type), new_range));
+    else
+        return new_range;
+}
+
+/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
+unsigned get_arity(expr type) {
+    unsigned r = 0;
+    while (is_pi(type)) {
+        type = binding_body(type);
+        r++;
+    }
+    return r;
+}
+
+expr mk_aux_type_metavar_for(expr const & t) {
+    expr new_type = replace_range(t, mk_sort(mk_meta_univ(mk_fresh_name())));
+    name n        = mk_fresh_name();
+    return mk_metavar(n, new_type);
+}
+
+expr mk_aux_metavar_for(expr const & t) {
+    unsigned num  = get_arity(t);
+    expr r        = mk_app_vars(mk_aux_type_metavar_for(t), num);
+    expr new_type = replace_range(t, r);
+    name n        = mk_fresh_name();
+    return mk_metavar(n, new_type);
+}
+
+expr mk_pi_for(expr const & meta) {
+    lean_assert(is_meta(meta));
+    buffer<expr> margs;
+    expr const & m     = get_app_args(meta, margs);
+    expr const & mtype = mlocal_type(m);
+    expr maux1         = mk_aux_type_metavar_for(mtype);
+    expr dontcare;
+    expr tmp_pi        = mk_pi(mk_fresh_name(), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context
+    expr mtype2        = replace_range(mtype, tmp_pi); // trick for "extending" the context
+    expr maux2         = mk_aux_type_metavar_for(mtype2);
+    expr A             = mk_app(maux1, margs);
+    margs.push_back(Var(0));
+    expr B             = mk_app(maux2, margs);
+    return mk_pi(mk_fresh_name(), A, B);
+}
+
+#endif
+
+optional<expr> old_type_checker::expand_macro(expr const & m) {
+    lean_assert(is_macro(m));
+    return macro_def(m).expand(m, m_old_tc_ctx);
+}
+
+/**
+   \brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
+   It also returns the fresh local constant.
+*/
+pair<expr, expr> old_type_checker::open_binding_body(expr const & e) {
+    expr local     = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e));
+    return mk_pair(instantiate(binding_body(e), local), local);
+}
+
+constraint old_type_checker::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+    return ::lean::mk_eq_cnstr(lhs, rhs, j);
+}
+
+/**
+   \brief Make sure \c e "is" a sort, and return the corresponding sort.
+   If \c e is not a sort, then the whnf procedure is invoked. Then, there are
+   two options: the normalize \c e is a sort, or it is a meta. If it is a meta,
+   a new constraint is created forcing it to be a sort.
+
+   \remark \c s is used to extract position (line number information) when an
+   error message is produced
+*/
+pair<expr, constraint_seq> old_type_checker::ensure_sort_core(expr e, expr const & s) {
+    if (is_sort(e))
+        return to_ecs(e);
+    auto ecs = whnf(e);
+    if (is_sort(ecs.first)) {
+        return ecs;
+    } else if (is_meta(ecs.first)) {
+        expr r = mk_sort(mk_meta_univ(mk_fresh_name()));
+        justification j = mk_justification(s,
+                                           [=](formatter const & fmt, substitution const & subst, bool) {
+                                               return pp_type_expected(fmt, substitution(subst).instantiate(s));
+                                           });
+        return to_ecs(r, mk_eq_cnstr(ecs.first, r, j), ecs.second);
+    } else {
+        throw_kernel_exception(m_env, s, [=](formatter const & fmt) { return pp_type_expected(fmt, s); });
+    }
+}
+
+/** \brief Similar to \c ensure_sort, but makes sure \c e "is" a Pi. */
+pair<expr, constraint_seq> old_type_checker::ensure_pi_core(expr e, expr const & s) {
+    if (is_pi(e))
+        return to_ecs(e);
+    auto ecs = whnf(e);
+    if (is_pi(ecs.first)) {
+        return ecs;
+    } else if (auto m = is_stuck(ecs.first)) {
+        expr r             = mk_pi_for(*m);
+        justification j    = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) {
+                return pp_function_expected(fmt, substitution(subst).instantiate(s));
+            });
+        return to_ecs(r, mk_eq_cnstr(ecs.first, r, j), ecs.second);
+    } else {
+        throw_kernel_exception(m_env, s, [=](formatter const & fmt) { return pp_function_expected(fmt, s); });
+    }
+}
+
+static constexpr char const * g_macro_error_msg = "failed to type check macro expansion";
+
+justification old_type_checker::mk_macro_jst(expr const & e) {
+    return mk_justification(e, [=](formatter const &, substitution const &, bool) {
+            return format(g_macro_error_msg);
+        });
+}
+
+void old_type_checker::check_level(level const & l, expr const & s) {
+    if (auto n1 = get_undef_global(l, m_env))
+        throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'", s);
+    if (m_params) {
+        if (auto n2 = get_undef_param(l, *m_params))
+            throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '"
+                                   << *n2 << "'", s);
+    }
+}
+
+old_app_delayed_justification::old_app_delayed_justification(expr const & e, expr const & arg, expr const & f_type,
+                                                     expr const & a_type):
+    m_e(e), m_arg(arg), m_fn_type(f_type), m_arg_type(a_type) {}
+
+justification mk_app_justification(expr const & e, expr const & fn_type, expr const & arg, expr const & a_type) {
+    auto pp_fn = [=](formatter const & fmt, substitution const & subst, bool as_error) {
+        substitution s(subst);
+        return pp_app_type_mismatch(fmt, s.instantiate(e), s.instantiate(fn_type), s.instantiate(arg), s.instantiate(a_type), as_error);
+    };
+    return mk_justification(e, pp_fn);
+}
+
+justification old_app_delayed_justification::get() {
+    if (!m_jst) {
+        // We should not have a reference to this object inside the closure.
+        // So, we create the following locals that will be captured by the closure instead of 'this'.
+        m_jst = mk_app_justification(m_e, m_fn_type, m_arg, m_arg_type);
+    }
+    return *m_jst;
+}
+
+expr old_type_checker::infer_constant(expr const & e, bool infer_only) {
+    declaration d    = m_env.get(const_name(e));
+    auto const & ps = d.get_univ_params();
+    auto const & ls = const_levels(e);
+    if (length(ps) != length(ls))
+        throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '"
+                               << const_name(e) << "', #"
+                               << length(ps)  << " expected, #" << length(ls) << " provided");
+    if (!infer_only) {
+        for (level const & l : ls)
+            check_level(l, e);
+    }
+    return instantiate_type_univ_params(d, ls);
+}
+
+pair<expr, constraint_seq> old_type_checker::infer_macro(expr const & e, bool infer_only) {
+    auto def = macro_def(e);
+    pair<expr, constraint_seq> tcs = def.check_type(e, m_old_tc_ctx, infer_only);
+    expr t            = tcs.first;
+    constraint_seq cs = tcs.second;
+    if (!infer_only && def.trust_level() >= m_env.trust_lvl()) {
+        throw_kernel_exception(m_env, "declaration contains macro with trust-level higher than the one allowed "
+                               "(possible solution: unfold macro, or increase trust-level)", e);
+    }
+    return mk_pair(t, cs);
+}
+
+pair<expr, constraint_seq> old_type_checker::infer_lambda(expr const & _e, bool infer_only) {
+    buffer<expr> es, ds, ls;
+    expr e = _e;
+    constraint_seq cs;
+    while (is_lambda(e)) {
+        es.push_back(e);
+        ds.push_back(binding_domain(e));
+        expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
+        expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e));
+        ls.push_back(l);
+        if (!infer_only) {
+            pair<expr, constraint_seq> dtcs = infer_type_core(d, infer_only);
+            pair<expr, constraint_seq> scs  = ensure_sort_core(dtcs.first, d);
+            cs = cs + scs.second + dtcs.second;
+        }
+        e = binding_body(e);
+    }
+    pair<expr, constraint_seq> rcs = infer_type_core(instantiate_rev(e, ls.size(), ls.data()), infer_only);
+    cs = cs + rcs.second;
+    expr r = abstract_locals(rcs.first, ls.size(), ls.data());
+    unsigned i = es.size();
+    while (i > 0) {
+        --i;
+        r = mk_pi(binding_name(es[i]), ds[i], r, binding_info(es[i]));
+    }
+    return mk_pair(r, cs);
+}
+
+pair<expr, constraint_seq> old_type_checker::infer_pi(expr const & _e, bool infer_only) {
+    buffer<expr>  ls;
+    buffer<level> us;
+    expr e = _e;
+    constraint_seq cs;
+    while (is_pi(e)) {
+        expr d                          = instantiate_rev(binding_domain(e), ls.size(), ls.data());
+        pair<expr, constraint_seq> dtcs = infer_type_core(d, infer_only);
+        pair<expr, constraint_seq> scs  = ensure_sort_core(dtcs.first, d);
+        cs = cs + scs.second + dtcs.second;
+        expr t1 = scs.first;
+        us.push_back(sort_level(t1));
+        expr l  = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e));
+        ls.push_back(l);
+        e = binding_body(e);
+    }
+    e = instantiate_rev(e, ls.size(), ls.data());
+    pair<expr, constraint_seq> etcs = infer_type_core(e, infer_only);
+    pair<expr, constraint_seq> scs  = ensure_sort_core(etcs.first, e);
+    cs = cs + scs.second + etcs.second;
+    level r = sort_level(scs.first);
+    unsigned i = ls.size();
+    while (i > 0) {
+        --i;
+        r = m_env.impredicative() ? mk_imax(us[i], r) : mk_max(us[i], r);
+    }
+    return mk_pair(mk_sort(r), cs);
+}
+
+pair<expr, constraint_seq> old_type_checker::infer_app(expr const & e, bool infer_only) {
+    if (!infer_only) {
+        pair<expr, constraint_seq> ftcs = infer_type_core(app_fn(e), infer_only);
+        pair<expr, constraint_seq> pics = ensure_pi_core(ftcs.first, e);
+        expr f_type = pics.first;
+        pair<expr, constraint_seq> acs  = infer_type_core(app_arg(e), infer_only);
+        expr a_type = acs.first;
+        old_app_delayed_justification jst(e, app_arg(e), f_type, a_type);
+        expr d_type = binding_domain(f_type);
+        pair<bool, constraint_seq> dcs  = is_def_eq(a_type, d_type, jst);
+        if (!dcs.first) {
+            throw_kernel_exception(m_env, e,
+                                   [=](formatter const & fmt) {
+                                       return pp_app_type_mismatch(fmt, e, f_type, app_arg(e), a_type, true);
+                                   });
+        }
+        return mk_pair(instantiate(binding_body(f_type), app_arg(e)),
+                       pics.second + ftcs.second + dcs.second + acs.second);
+    } else {
+        buffer<expr> args;
+        expr const & f = get_app_args(e, args);
+        pair<expr, constraint_seq> ftcs = infer_type_core(f, true);
+        expr f_type       = ftcs.first;
+        constraint_seq cs = ftcs.second;
+        unsigned j        = 0;
+        unsigned nargs    = args.size();
+        for (unsigned i = 0; i < nargs; i++) {
+            if (is_pi(f_type)) {
+                f_type = binding_body(f_type);
+            } else {
+                f_type = instantiate_rev(f_type, i-j, args.data()+j);
+                pair<expr, constraint_seq> pics = ensure_pi_core(f_type, e);
+                f_type = pics.first;
+                cs     = pics.second + cs;
+                f_type = binding_body(f_type);
+                j = i;
+            }
+        }
+        expr r = instantiate_rev(f_type, nargs-j, args.data()+j);
+        return mk_pair(r, cs);
+    }
+}
+
+pair<expr, constraint_seq> old_type_checker::infer_let(expr const & e, bool infer_only) {
+    if (!infer_only) {
+        pair<expr, constraint_seq> dtcs = infer_type_core(let_type(e), infer_only);
+        pair<expr, constraint_seq> scs  = ensure_sort_core(dtcs.first, e);
+        pair<expr, constraint_seq> vcs  = infer_type_core(let_value(e), infer_only);
+        expr v_type = vcs.first;
+        // TODO(Leo): we will remove justifications in the future.
+        as_delayed_justification jst(mk_justification("let mismatch"));
+        pair<bool, constraint_seq> dcs  = is_def_eq(v_type, let_type(e), jst);
+        if (!dcs.first) {
+            throw_kernel_exception(m_env, e,
+                                   [=](formatter const & fmt) {
+                                       return pp_def_type_mismatch(fmt, let_name(e), let_type(e), v_type, true);
+                                   });
+        }
+    }
+    return infer_type_core(instantiate(let_body(e), let_value(e)), infer_only);
+}
+
+expr old_type_checker::infer_type_core(expr const & e, bool infer_only, constraint_seq & cs) {
+    auto r = infer_type_core(e, infer_only);
+    cs = cs + r.second;
+    return r.first;
+}
+
+/**
+   \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
+
+   \pre closed(e)
+*/
+pair<expr, constraint_seq> old_type_checker::infer_type_core(expr const & e, bool infer_only) {
+    if (is_var(e))
+        throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e);
+
+    lean_assert(closed(e));
+    check_system("type checker");
+
+    if (m_memoize) {
+        auto it = m_infer_type_cache[infer_only].find(e);
+        if (it != m_infer_type_cache[infer_only].end())
+            return it->second;
+    }
+
+    pair<expr, constraint_seq> r;
+    switch (e.kind()) {
+    case expr_kind::Local: case expr_kind::Meta:  r.first = mlocal_type(e);  break;
+    case expr_kind::Var:
+        lean_unreachable();  // LCOV_EXCL_LINE
+    case expr_kind::Sort:
+        if (!infer_only) check_level(sort_level(e), e);
+        r.first = mk_sort(mk_succ(sort_level(e)));
+        break;
+    case expr_kind::Constant:  r.first = infer_constant(e, infer_only); break;
+    case expr_kind::Macro:     r = infer_macro(e, infer_only);          break;
+    case expr_kind::Lambda:    r = infer_lambda(e, infer_only);         break;
+    case expr_kind::Pi:        r = infer_pi(e, infer_only);             break;
+    case expr_kind::App:       r = infer_app(e, infer_only);            break;
+    case expr_kind::Let:       r = infer_let(e, infer_only);            break;
+    }
+
+    if (m_memoize)
+        m_infer_type_cache[infer_only].insert(mk_pair(e, r));
+
+    return r;
+}
+
+pair<expr, constraint_seq> old_type_checker::infer_type(expr const & e) {
+    return infer_type_core(e, true);
+}
+
+pair<expr, constraint_seq> old_type_checker::check(expr const & e, level_param_names const & ps) {
+    flet<level_param_names const *> updt(m_params, &ps);
+    return infer_type_core(e, false);
+}
+
+pair<expr, constraint_seq> old_type_checker::check_ignore_undefined_universes(expr const & e) {
+    flet<level_param_names const *> updt(m_params, nullptr);
+    return infer_type_core(e, false);
+}
+
+pair<expr, constraint_seq> old_type_checker::ensure_sort(expr const & e, expr const & s) {
+    return ensure_sort_core(e, s);
+}
+
+pair<expr, constraint_seq> old_type_checker::ensure_pi(expr const & e, expr const & s) {
+    return ensure_pi_core(e, s);
+}
+
+/** \brief Return true iff \c t and \c s are definitionally equal */
+pair<bool, constraint_seq> old_type_checker::is_def_eq(expr const & t, expr const & s, delayed_justification & jst) {
+    return m_conv->is_def_eq(t, s, *this, jst);
+}
+
+pair<bool, constraint_seq> old_type_checker::is_def_eq(expr const & t, expr const & s) {
+    return m_conv->is_def_eq(t, s, *this);
+}
+
+pair<bool, constraint_seq> old_type_checker::is_def_eq(expr const & t, expr const & s, justification const & j) {
+    as_delayed_justification djst(j);
+    return is_def_eq(t, s, djst);
+}
+
+pair<bool, constraint_seq> old_type_checker::is_def_eq_types(expr const & t, expr const & s, justification const & j) {
+    auto tcs1 = infer_type_core(t, true);
+    auto tcs2 = infer_type_core(s, true);
+    as_delayed_justification djst(j);
+    auto bcs  = m_conv->is_def_eq(tcs1.first, tcs2.first, *this, djst);
+    return mk_pair(bcs.first, bcs.first ? bcs.second + tcs1.second + tcs2.second : constraint_seq());
+}
+
+/** \brief Return true iff \c e is a proposition */
+pair<bool, constraint_seq> old_type_checker::is_prop(expr const & e) {
+    if (m_env.impredicative()) {
+        auto tcs  = infer_type(e);
+        auto wtcs = whnf(tcs.first);
+        bool r    = wtcs.first == mk_Prop();
+        if (r)
+            return mk_pair(true, tcs.second + wtcs.second);
+        else
+            return mk_pair(false, constraint_seq());
+    } else {
+        return mk_pair(false, constraint_seq());
+    }
+}
+
+pair<expr, constraint_seq> old_type_checker::whnf(expr const & t) {
+    return m_conv->whnf(t, *this);
+}
+
+bool old_type_checker::is_opaque(declaration const & d) const {
+    return m_conv->is_opaque(d);
+}
+
+bool old_type_checker::is_opaque(expr const & c) const {
+    lean_assert(is_constant(c));
+    if (auto d = m_env.find(const_name(c)))
+        return d->is_definition() && is_opaque(*d);
+    else
+        return true;
+}
+
+old_type_checker::old_type_checker(environment const & env, std::unique_ptr<old_converter> && conv, bool memoize):
+    m_env(env), m_conv(std::move(conv)), m_old_tc_ctx(*this), m_tc_ctx(*this),
+    m_memoize(memoize), m_params(nullptr) {
+}
+
+old_type_checker::old_type_checker(environment const & env, bool memoize):
+    old_type_checker(env, std::unique_ptr<old_converter>(new old_default_converter(env, memoize)), memoize) {}
+
+old_type_checker::~old_type_checker() {}
+
+optional<expr> old_type_checker::is_stuck(expr const & e) {
+    return m_conv->is_stuck(e, *this);
+}
+
+void initialize_old_type_checker() {
+}
+
+void finalize_old_type_checker() {
+}
+}
diff --git a/src/library/old_type_checker.h b/src/library/old_type_checker.h
new file mode 100644
index 0000000000..0ef392be2d
--- /dev/null
+++ b/src/library/old_type_checker.h
@@ -0,0 +1,283 @@
+/*
+Copyright (c) 2013-14 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 <utility>
+#include <algorithm>
+#include "util/flet.h"
+#include "util/name_set.h"
+#include "util/fresh_name.h"
+#include "kernel/environment.h"
+#include "kernel/constraint.h"
+#include "kernel/justification.h"
+#include "kernel/expr_maps.h"
+#include "kernel/type_checker.h"
+#include "kernel/abstract_type_context.h"
+#include "library/old_converter.h"
+
+namespace lean {
+/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
+unsigned get_arity(expr type);
+
+#if 0
+inline pair<expr, constraint_seq> to_ecs(expr const & e) { return mk_pair(e, empty_cs()); }
+inline pair<expr, constraint_seq> to_ecs(expr const & e, constraint const & c, constraint_seq const & cs) {
+    return mk_pair(e, constraint_seq(constraint_seq(c), cs));
+}
+inline pair<expr, constraint_seq> to_ecs(expr const & e, constraint const & c) { return mk_pair(e, constraint_seq(c)); }
+inline pair<expr, constraint_seq> to_ecs(expr const & e, constraint_seq const & cs) { return mk_pair(e, cs); }
+#endif
+
+/** \brief Given \c type of the form <tt>(Pi ctx, r)</tt>, return <tt>(Pi ctx, new_range)</tt> */
+expr replace_range(expr const & type, expr const & new_range);
+
+/**
+   \brief Given a type \c t of the form
+      <tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
+   return a new metavariable \c m1 with type
+      <tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u}</tt>
+   where \c u is a new universe metavariable.
+*/
+expr mk_aux_type_metavar_for(expr const & t);
+
+/**
+   \brief Given a type \c t of the form
+      <tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
+   return a new metavariable \c m1 with type
+      <tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), (?m2 x_1 ... x_n)</tt>
+   where \c ?m2 is a new metavariable with type
+      <tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u}</tt>
+   where \c u is a new universe metavariable.
+*/
+expr mk_aux_metavar_for(expr const & t);
+
+/**
+   \brief Given a meta (?m t_1 ... t_n) where ?m has type
+      <tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
+   return a Pi term
+      <tt>Pi (x : ?m1 t_1 ... t_n), (?m2 t_1 ... t_n x) </tt>
+   where ?m1 and ?m2 are fresh metavariables
+*/
+expr mk_pi_for(expr const & meta);
+
+/**
+   \brief Lean Type Checker. It can also be used to infer types, check whether a
+   type \c A is convertible to a type \c B, etc.
+
+   The type checker produces constraints, and they are sent to the constraint handler.
+*/
+class old_type_checker {
+    typedef expr_bi_struct_map<pair<expr, constraint_seq>> cache;
+
+    /** \brief Interface old_type_checker <-> macro & normalizer_extension
+        TODO(Leo): delete this class. It will be subsumed by old_type_checker_context. */
+    class old_type_checker_context : public extension_context {
+        old_type_checker & m_tc;
+    public:
+        old_type_checker_context(old_type_checker & tc):m_tc(tc) {}
+        virtual environment const & env() const { return m_tc.m_env; }
+        virtual pair<expr, constraint_seq> whnf(expr const & e) { return m_tc.whnf(e); }
+        virtual pair<bool, constraint_seq> is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) {
+            return m_tc.is_def_eq(e1, e2, j);
+        }
+        virtual pair<expr, constraint_seq> check_type(expr const & e, bool infer_only) {
+            return m_tc.infer_type_core(e, infer_only);
+        }
+        virtual optional<expr> is_stuck(expr const & e) { return m_tc.is_stuck(e); }
+    };
+
+    class type_checker_context : public abstract_type_context {
+        old_type_checker & m_tc;
+    public:
+        type_checker_context(old_type_checker & tc):m_tc(tc) {}
+        virtual environment const & env() const { return m_tc.m_env; }
+        virtual expr whnf(expr const & e) { return m_tc.whnf(e).first; }
+        virtual bool is_def_eq(expr const & e1, expr const & e2) {
+            no_delayed_justification j;
+            return m_tc.is_def_eq(e1, e2, j).first;
+        }
+        virtual expr infer(expr const & e) { return m_tc.infer_type_core(e, true).first; }
+        virtual expr check(expr const & e) { return m_tc.infer_type_core(e, false).first; }
+        virtual optional<expr> is_stuck(expr const & e) { return m_tc.is_stuck(e); }
+    };
+
+    environment                    m_env;
+    std::unique_ptr<old_converter> m_conv;
+    // In the type checker cache, we must take into account binder information.
+    // Examples:
+    // The type of (lambda x : A, t)   is (Pi x : A, typeof(t))
+    // The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t))
+    cache                      m_infer_type_cache[2];
+    old_type_checker_context   m_old_tc_ctx;
+    type_checker_context       m_tc_ctx;
+    bool                       m_memoize;
+    // temp flag
+    level_param_names const *  m_params;
+
+    friend class old_converter; // allow converter to access the following methods
+    pair<expr, expr> open_binding_body(expr const & e);
+    pair<expr, constraint_seq> ensure_sort_core(expr e, expr const & s);
+    pair<expr, constraint_seq> ensure_pi_core(expr e, expr const & s);
+    justification mk_macro_jst(expr const & e);
+    void check_level(level const & l, expr const & s);
+    expr infer_constant(expr const & e, bool infer_only);
+    pair<expr, constraint_seq> infer_macro(expr const & e, bool infer_only);
+    pair<expr, constraint_seq> infer_lambda(expr const & e, bool infer_only);
+    pair<expr, constraint_seq> infer_pi(expr const & e, bool infer_only);
+    pair<expr, constraint_seq> infer_app(expr const & e, bool infer_only);
+    pair<expr, constraint_seq> infer_let(expr const & e, bool infer_only);
+    pair<expr, constraint_seq> infer_type_core(expr const & e, bool infer_only);
+    pair<expr, constraint_seq> infer_type(expr const & e);
+    expr infer_type_core(expr const & e, bool infer_only, constraint_seq & cs);
+
+    extension_context & get_extension() { return m_old_tc_ctx; }
+    constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+public:
+    /**
+       \brief Create a type checker for the given environment. The auxiliary names created by this
+       type checker are based on the given name generator.
+
+       memoize: if true, then inferred types are memoized/cached
+    */
+    old_type_checker(environment const & env, std::unique_ptr<old_converter> && conv, bool memoize = true);
+    old_type_checker(environment const & env, bool memoize = true);
+    ~old_type_checker();
+
+    environment const & env() const { return m_env; }
+
+    abstract_type_context & get_type_context() { return m_tc_ctx; }
+
+    /**
+       \brief Return the type of \c t.
+
+       It does not check whether the input expression is type correct or not.
+       The contract is: IF the input expression is type correct, then the inferred
+       type is correct.
+       Throw an exception if a type error is found.
+
+       The result is meaningful only if the generated constraints can be solved.
+   */
+    pair<expr, constraint_seq> infer(expr const & t) { return infer_type(t); }
+
+    /**
+       \brief Type check the given expression, and return the type of \c t.
+       Throw an exception if a type error is found.
+
+       The result is meaningful only if the generated constraints can be solved.
+    */
+    pair<expr, constraint_seq> check(expr const & t, level_param_names const & ps = level_param_names());
+    /** \brief Like \c check, but ignores undefined universes */
+    pair<expr, constraint_seq> check_ignore_undefined_universes(expr const & e);
+
+    /** \brief Return true iff t is definitionally equal to s. */
+    pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);
+    pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, justification const & j);
+    pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, delayed_justification & jst);
+    /** \brief Return true iff types of \c t and \c s are (may be) definitionally equal (modulo constraints) */
+    pair<bool, constraint_seq> is_def_eq_types(expr const & t, expr const & s, justification const & j);
+    /** \brief Return true iff t is a proposition. */
+    pair<bool, constraint_seq> is_prop(expr const & t);
+    /** \brief Return the weak head normal form of \c t. */
+    pair<expr, constraint_seq> whnf(expr const & t);
+    /** \brief Return a Pi if \c t is convertible to a Pi type. Throw an exception otherwise.
+        The argument \c s is used when reporting errors */
+    pair<expr, constraint_seq> ensure_pi(expr const & t, expr const & s);
+    pair<expr, constraint_seq> ensure_pi(expr const & t) { return ensure_pi(t, t); }
+    /** \brief Mare sure type of \c e is a Pi, and return it. Throw an exception otherwise. */
+    pair<expr, constraint_seq> ensure_fun(expr const & e) {
+        auto tcs  = infer(e);
+        auto pics = ensure_pi(tcs.first, e);
+        return mk_pair(pics.first, pics.second + tcs.second);
+    }
+    /** \brief Return a Sort if \c t is convertible to Sort. Throw an exception otherwise.
+        The argument \c s is used when reporting errors. */
+    pair<expr, constraint_seq> ensure_sort(expr const & t, expr const & s);
+    /** \brief Return a Sort if \c t is convertible to Sort. Throw an exception otherwise. */
+    pair<expr, constraint_seq> ensure_sort(expr const & t) { return ensure_sort(t, t); }
+    /** \brief Mare sure type of \c e is a sort, and return it. Throw an exception otherwise. */
+    pair<expr, constraint_seq> ensure_type(expr const & e) {
+        auto tcs = infer(e);
+        auto scs = ensure_sort(tcs.first, e);
+        return mk_pair(scs.first, scs.second + tcs.second);
+    }
+
+    expr whnf(expr const & e, constraint_seq & cs) { auto r = whnf(e); cs += r.second; return r.first; }
+    expr infer(expr const & e, constraint_seq & cs) { auto r = infer(e); cs += r.second; return r.first; }
+    expr ensure_pi(expr const & e, constraint_seq & cs) { auto r = ensure_pi(e); cs += r.second; return r.first; }
+    expr ensure_pi(expr const & e, expr const & s, constraint_seq & cs) { auto r = ensure_pi(e, s); cs += r.second; return r.first; }
+    expr ensure_sort(expr const & t, expr const & s, constraint_seq & cs) { auto r = ensure_sort(t, s); cs += r.second; return r.first; }
+    expr ensure_type(expr const & e, constraint_seq & cs) { auto r = ensure_type(e); cs += r.second; return r.first; }
+
+    bool is_def_eq(expr const & t, expr const & s, justification const & j, constraint_seq & cs) {
+        auto r = is_def_eq(t, s, j);
+        if (r.first)
+            cs = r.second + cs;
+        return r.first;
+    }
+
+    bool is_def_eq_types(expr const & t, expr const & s, justification const & j, constraint_seq & cs) {
+        auto r = is_def_eq_types(t, s, j);
+        if (r.first)
+            cs = r.second + cs;
+        return r.first;
+    }
+    bool is_prop(expr const & t, constraint_seq & cs) {
+        auto r = is_prop(t);
+        if (r.first)
+            cs += r.second;
+        return r.first;
+    }
+
+    optional<expr> expand_macro(expr const & m);
+
+    /** \brief Return true iff \c d is opaque with respect to this type checker. */
+    bool is_opaque(declaration const & d) const;
+    /** \brief Return true iff the constant \c c is opaque with respect to this type checker. */
+    bool is_opaque(expr const & c) const;
+
+    /** \brief Return a metavariable that may be stucking the \c e's reduction. */
+    optional<expr> is_stuck(expr const & e);
+
+    optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); }
+
+    bool may_reduce_later(expr const & e) { return !is_meta(e) && static_cast<bool>(m_conv->is_stuck(e, *this)); }
+
+    template<typename F>
+    typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
+        flet<level_param_names const *> updt(m_params, &ps);
+        return f();
+    }
+};
+
+typedef std::shared_ptr<old_type_checker> old_type_checker_ref;
+
+void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type);
+
+/**
+    \brief Create a justification for an application \c e where the expected type must be \c d_type and
+    the argument type is \c a_type.
+*/
+justification mk_app_justification(expr const & e, expr const & arg, expr const & d_type, expr const & a_type);
+
+/**
+   \brief Create a justification for a application type mismatch,
+   \c e is the application, \c fn_type and \c arg_type are the function and argument type.
+*/
+class old_app_delayed_justification : public delayed_justification {
+    expr const & m_e;
+    expr const & m_arg;
+    expr const & m_fn_type;
+    expr const & m_arg_type;
+    optional<justification> m_jst;
+public:
+    old_app_delayed_justification(expr const & e, expr const & arg, expr const & f_type, expr const & a_type);
+    virtual justification get();
+};
+
+void initialize_old_type_checker();
+void finalize_old_type_checker();
+}
diff --git a/src/library/projection.cpp b/src/library/projection.cpp
index 10cf716680..e5fc4b2afd 100644
--- a/src/library/projection.cpp
+++ b/src/library/projection.cpp
@@ -130,7 +130,7 @@ optional<pair<expr, constraint_seq>> projection_converter::norm_ext(expr const &
     if (auto r = reduce_projection(e)) {
         return r;
     } else {
-        return default_converter::norm_ext(e);
+        return old_default_converter::norm_ext(e);
     }
 }
 
@@ -146,7 +146,7 @@ bool projection_converter::postpone_is_def_eq(expr const & t, expr const & s) {
         if (it2 && is_stuck(s, *m_tc))
             return true;
     }
-    return default_converter::postpone_is_def_eq(t, s);
+    return old_default_converter::postpone_is_def_eq(t, s);
 }
 
 // Apply lazy delta-reduction and then normalizer extensions
@@ -197,10 +197,10 @@ lbool projection_converter::reduce_def_eq(expr & t_n, expr & s_n, constraint_seq
     }
 }
 
-optional<expr> projection_converter::is_stuck(expr const & e, type_checker & c) {
+optional<expr> projection_converter::is_stuck(expr const & e, old_type_checker & c) {
     projection_info const * info = is_projection(e);
     if (!info)
-        return default_converter::is_stuck(e, c);
+        return old_default_converter::is_stuck(e, c);
     buffer<expr> args;
     get_app_args(e, args);
     if (args.size() <= info->m_nparams)
@@ -210,7 +210,7 @@ optional<expr> projection_converter::is_stuck(expr const & e, type_checker & c)
 }
 
 projection_converter::projection_converter(environment const & env):
-    default_converter(env, true) {
+    old_default_converter(env, true) {
     m_proj_info = ::lean::get_extension(env).m_info;
 }
 
diff --git a/src/library/projection.h b/src/library/projection.h
index bc18c1de5c..83c9c5f9d9 100644
--- a/src/library/projection.h
+++ b/src/library/projection.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
-#include "kernel/default_converter.h"
+#include "library/old_default_converter.h"
 
 namespace lean {
 /** \brief Auxiliary information attached to projections. This information
@@ -58,7 +58,7 @@ name_map<projection_info> const & get_projection_info_map(environment const & en
 */
 bool is_structure_like(environment const & env, name const & S);
 
-class projection_converter : public default_converter {
+class projection_converter : public old_default_converter {
     name_map<projection_info> m_proj_info;
     projection_info const * is_projection(expr const & e) const;
     optional<pair<expr, constraint_seq>> reduce_projection(expr const & t);
@@ -68,7 +68,7 @@ class projection_converter : public default_converter {
 public:
     projection_converter(environment const & env);
     virtual bool is_opaque(declaration const & d) const;
-    virtual optional<expr> is_stuck(expr const & e, type_checker & c);
+    virtual optional<expr> is_stuck(expr const & e, old_type_checker & c);
 };
 
 void initialize_projection();
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index 3adfb9c5eb..7c92ece723 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -131,7 +131,7 @@ name_predicate mk_irreducible_pred(environment const & env) {
     };
 }
 
-type_checker_ptr mk_type_checker(environment const & env, reducible_behavior rb) {
+old_type_checker_ptr mk_type_checker(environment const & env, reducible_behavior rb) {
     switch (rb) {
     case UnfoldReducible:
         return mk_type_checker(env, mk_not_reducible_pred(env));
@@ -141,7 +141,7 @@ type_checker_ptr mk_type_checker(environment const & env, reducible_behavior rb)
     lean_unreachable();
 }
 
-type_checker_ptr mk_opaque_type_checker(environment const & env) {
+old_type_checker_ptr mk_opaque_type_checker(environment const & env) {
     return mk_type_checker(env, [](name const &) { return true; });
 }
 }
diff --git a/src/library/reducible.h b/src/library/reducible.h
index bbb7745768..85f81ecf93 100644
--- a/src/library/reducible.h
+++ b/src/library/reducible.h
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
-#include "kernel/type_checker.h"
 #include "library/util.h"
 
 namespace lean {
@@ -38,10 +37,10 @@ name_predicate mk_irreducible_pred(environment const & env);
 enum reducible_behavior { UnfoldReducible, UnfoldSemireducible };
 
 /** \brief Create a type checker that takes the "reducibility" hints into account. */
-type_checker_ptr mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible);
+old_type_checker_ptr mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible);
 
 /** \brief Create a type checker that treats all definitions as opaque. */
-type_checker_ptr mk_opaque_type_checker(environment const & env);
+old_type_checker_ptr mk_opaque_type_checker(environment const & env);
 
 void initialize_reducible();
 void finalize_reducible();
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index a66ad462e1..b1e6d80505 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -14,13 +14,13 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/error_msgs.h"
-#include "kernel/type_checker.h"
 #include "library/reducible.h"
 #include "library/unifier.h"
 #include "library/occurs.h"
 #include "library/constants.h"
 #include "library/type_util.h"
 #include "library/class_instance_resolution.h"
+#include "library/old_type_checker.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/apply_tactic.h"
 
@@ -76,7 +76,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
         return proof_state_seq();
     }
     bool class_inst   = get_apply_class_instance(ios.get_options());
-    std::shared_ptr<type_checker> tc(mk_type_checker(env));
+    std::shared_ptr<old_type_checker> tc(mk_type_checker(env));
     goal  g           = head(gs);
     goals tail_gs     = tail(gs);
     expr  t           = g.get_type();
@@ -235,19 +235,19 @@ void initialize_apply_tactic() {
                          "resolution for instance implicit arguments");
 
     register_tac(get_tactic_apply_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument");
                      return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
                  });
 
     register_tac(get_tactic_eapply_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'eapply' tactic, invalid argument");
                      return eapply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
                  });
 
     register_tac(get_tactic_fapply_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'fapply' tactic, invalid argument");
                      return fapply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
                  });
diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/tactic/assert_tactic.cpp
index a2d2286633..26e653712e 100644
--- a/src/library/tactic/assert_tactic.cpp
+++ b/src/library/tactic/assert_tactic.cpp
@@ -50,7 +50,7 @@ tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e)
 
 void initialize_assert_tactic() {
     register_tac(get_tactic_assert_hypothesis_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'assert' tactic, argument must be an identifier");
                      check_tactic_expr(app_arg(e), "invalid 'assert' tactic, argument must be an expression");
                      return assert_tactic(fn, id, get_tactic_expr_expr(app_arg(e)));
diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp
index c9b0fb370b..1a45edc521 100644
--- a/src/library/tactic/change_tactic.cpp
+++ b/src/library/tactic/change_tactic.cpp
@@ -71,7 +71,7 @@ tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) {
 
 void initialize_change_tactic() {
     register_tac(get_tactic_change_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'change' tactic, invalid argument");
                      return change_goal_tactic(fn, get_tactic_expr_expr(app_arg(e)));
                  });
diff --git a/src/library/tactic/check_expr_tactic.cpp b/src/library/tactic/check_expr_tactic.cpp
index 8117495cdf..56899df5d6 100644
--- a/src/library/tactic/check_expr_tactic.cpp
+++ b/src/library/tactic/check_expr_tactic.cpp
@@ -37,7 +37,7 @@ tactic check_expr_tactic(elaborate_fn const & elab, expr const & e,
 
 void initialize_check_expr_tactic() {
     register_tac(get_tactic_check_expr_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
                      check_tactic_expr(app_arg(e), "invalid 'check_expr' tactic, invalid argument");
                      expr arg = get_tactic_expr_expr(app_arg(e));
                      if (p) {
diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp
index a4df2289cf..e4bd6584c3 100644
--- a/src/library/tactic/clear_tactic.cpp
+++ b/src/library/tactic/clear_tactic.cpp
@@ -55,7 +55,7 @@ tactic clear_tactic(name const & n) {
 }
 
 void initialize_clear_tactic() {
-    auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+    auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
         buffer<name> ns;
         get_tactic_id_list_elements(app_arg(e), ns, "invalid 'clears' tactic, list of identifiers expected");
         tactic r = clear_tactic(ns.back());
diff --git a/src/library/tactic/congruence_tactic.cpp b/src/library/tactic/congruence_tactic.cpp
index 8eda7de729..4050c8f91d 100644
--- a/src/library/tactic/congruence_tactic.cpp
+++ b/src/library/tactic/congruence_tactic.cpp
@@ -21,7 +21,7 @@ Author: Leonardo de Moura
 namespace lean {
 enum class congr_arg_kind { Fixed, Singleton, Eq };
 
-optional<expr> mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios, expr const & fn, optional<unsigned> const & expected_num_args,
+optional<expr> mk_congr_subsingleton_thm(old_type_checker & tc, io_state const & ios, expr const & fn, optional<unsigned> const & expected_num_args,
                                          buffer<congr_arg_kind> & arg_kinds, constraint_seq & cs) {
     expr fn_type = tc.infer(fn, cs);
     buffer<expr> hyps;
diff --git a/src/library/tactic/constructor_tactic.cpp b/src/library/tactic/constructor_tactic.cpp
index ed35ec7d4f..ff4fde1383 100644
--- a/src/library/tactic/constructor_tactic.cpp
+++ b/src/library/tactic/constructor_tactic.cpp
@@ -108,29 +108,29 @@ tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, opti
 
 void initialize_constructor_tactic() {
     register_tac(name{"tactic", "constructor"},
-                 [](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      auto i = get_optional_unsigned(tc, app_arg(e));
                      return constructor_tactic(fn, i, optional<unsigned>(), list<expr>());
                  });
     register_tac(name{"tactic", "fconstructor"},
-                 [](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      auto i = get_optional_unsigned(tc, app_arg(e));
                      return constructor_tactic(fn, i, optional<unsigned>(), list<expr>(), true);
                  });
     register_tac(name{"tactic", "split"},
-                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
                      return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(1), list<expr>());
                  });
     register_tac(name{"tactic", "left"},
-                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
                      return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(2), list<expr>());
                  });
     register_tac(name{"tactic", "right"},
-                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
                      return constructor_tactic(fn, optional<unsigned>(2), optional<unsigned>(2), list<expr>());
                  });
     register_tac(name{"tactic", "existsi"},
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'existsi' tactic, invalid argument");
                      expr arg = get_tactic_expr_expr(app_arg(e));
                      return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(1), list<expr>(arg));
diff --git a/src/library/tactic/contradiction_tactic.cpp b/src/library/tactic/contradiction_tactic.cpp
index 07952c3efe..19bfba0656 100644
--- a/src/library/tactic/contradiction_tactic.cpp
+++ b/src/library/tactic/contradiction_tactic.cpp
@@ -84,7 +84,7 @@ tactic contradiction_tactic() {
 
 void initialize_contradiction_tactic() {
     register_tac(name{"tactic", "contradiction"},
-                 [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
                      list<name> empty;
                      return then(orelse(intros_tactic(empty), id_tactic()), contradiction_tactic());
                  });
diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp
index 04bf046f6d..45c63967a4 100644
--- a/src/library/tactic/exact_tactic.cpp
+++ b/src/library/tactic/exact_tactic.cpp
@@ -143,17 +143,17 @@ void initialize_exact_tactic() {
     g_rexact_tac_fn = new expr(Const(rexact_tac_name));
     g_refine_tac_fn = new expr(Const(refine_tac_name));
     register_tac(exact_tac_name,
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument");
                      return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true, false, false);
                  });
     register_tac(rexact_tac_name,
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'rexact' tactic, invalid argument");
                      return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false, false, false);
                  });
     register_tac(refine_tac_name,
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'refine' tactic, invalid argument");
                      return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true, true, false);
                  });
diff --git a/src/library/tactic/exfalso_tactic.cpp b/src/library/tactic/exfalso_tactic.cpp
index 786bebd038..890d7079a2 100644
--- a/src/library/tactic/exfalso_tactic.cpp
+++ b/src/library/tactic/exfalso_tactic.cpp
@@ -34,7 +34,7 @@ tactic exfalso_tactic() {
 }
 void initialize_exfalso_tactic() {
     register_tac(name{"tactic", "exfalso"},
-                 [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
                      return exfalso_tactic();
                  });
 }
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index 244f860b58..61a2b0517b 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -9,12 +9,12 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/optional.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
 #include "kernel/default_converter.h"
 #include "library/annotation.h"
 #include "library/string.h"
 #include "library/explicit.h"
 #include "library/placeholder.h"
+#include "library/old_type_checker.h"
 #include "library/num.h"
 #include "library/constants.h"
 #include "library/projection.h"
@@ -51,7 +51,7 @@ void register_tac(name const & n, expr_to_tactic_fn const & fn) {
 
 bool has_tactic_decls(environment const & env) {
     try {
-        type_checker tc(env);
+        old_type_checker tc(env);
         return
             tc.infer(*g_builtin_tac).first     == *g_tac_type &&
             tc.infer(*g_and_then_tac_fn).first == *g_tac_type >> (*g_tac_type >> *g_tac_type) &&
@@ -197,7 +197,7 @@ static bool is_builtin_tactic(expr const & v) {
         return false;
 }
 
-tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p) {
+tactic expr_to_tactic(old_type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p) {
     e = copy_tag(e, tc.whnf(e).first);
     expr f = get_app_fn(e);
     if (!is_constant(f))
@@ -236,7 +236,7 @@ tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_in
     }
 }
 
-unsigned get_unsigned(type_checker & tc, expr const & e, expr const & ref) {
+unsigned get_unsigned(old_type_checker & tc, expr const & e, expr const & ref) {
     optional<mpz> k = to_num(e);
     if (!k)
         k = to_num(tc.whnf(e).first);
@@ -249,7 +249,7 @@ unsigned get_unsigned(type_checker & tc, expr const & e, expr const & ref) {
     return k->get_unsigned_int();
 }
 
-unsigned get_unsigned_arg(type_checker & tc, expr const & e, unsigned i) {
+unsigned get_unsigned_arg(old_type_checker & tc, expr const & e, unsigned i) {
     buffer<expr> args;
     get_app_args(e, args);
     if (i >= args.size())
@@ -257,7 +257,7 @@ unsigned get_unsigned_arg(type_checker & tc, expr const & e, unsigned i) {
     return get_unsigned(tc, args[i], e);
 }
 
-optional<unsigned> get_optional_unsigned(type_checker & tc, expr const & e) {
+optional<unsigned> get_optional_unsigned(old_type_checker & tc, expr const & e) {
     if (is_app(e) && is_constant(get_app_fn(e))) {
         if (const_name(get_app_fn(e)) == get_option_some_name()) {
             return optional<unsigned>(get_unsigned(tc, app_arg(e), e));
@@ -286,7 +286,7 @@ public:
 
 tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
     bool memoize             = false;
-    type_checker tc(env, std::unique_ptr<converter>(new tac_builtin_opaque_converter(env)), memoize);
+    old_type_checker tc(env, std::unique_ptr<old_converter>(new tac_builtin_opaque_converter(env)), memoize);
     return expr_to_tactic(tc, fn, e, p);
 }
 
@@ -297,7 +297,7 @@ tactic fixpoint(expr const & b, elaborate_fn const & fn) {
 }
 
 void register_simple_tac(name const & n, std::function<tactic()> f) {
-    register_tac(n, [=](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+    register_tac(n, [=](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
             if (!is_constant(e))
                 throw expr_to_tactic_exception(e, "invalid constant tactic");
             return f();
@@ -305,7 +305,7 @@ void register_simple_tac(name const & n, std::function<tactic()> f) {
 }
 
 void register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f) {
-    register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
+    register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
             buffer<expr> args;
             get_app_args(e, args);
             if (args.size() != 2)
@@ -317,7 +317,7 @@ void register_bin_tac(name const & n, std::function<tactic(tactic const &, tacti
 }
 
 void register_unary_tac(name const & n, std::function<tactic(tactic const &)> f) {
-    register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
+    register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
             buffer<expr> args;
             get_app_args(e, args);
             if (args.size() != 1)
@@ -327,7 +327,7 @@ void register_unary_tac(name const & n, std::function<tactic(tactic const &)> f)
 }
 
 void register_unary_num_tac(name const & n, std::function<tactic(tactic const &, unsigned k)> f) {
-    register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
+    register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
             buffer<expr> args;
             get_app_args(e, args);
             if (args.size() != 2)
@@ -338,7 +338,7 @@ void register_unary_num_tac(name const & n, std::function<tactic(tactic const &,
 }
 
 void register_num_tac(name const & n, std::function<tactic(unsigned k)> f) {
-    register_tac(n, [=](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+    register_tac(n, [=](old_type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
             buffer<expr> args;
             get_app_args(e, args);
             if (args.size() != 1)
@@ -418,7 +418,7 @@ void initialize_expr_to_tactic() {
     register_num_tac(get_tactic_rotate_right_name(), [](unsigned k) { return rotate_right(k); });
 
     register_tac(get_tactic_fixpoint_name(),
-                 [](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      if (!is_constant(app_fn(e)))
                          throw expr_to_tactic_exception(e, "invalid fixpoint tactic, it must have one argument");
                      expr r = tc.whnf(mk_app(app_arg(e), e)).first;
diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h
index ddaa2d2545..0a945e9eda 100644
--- a/src/library/tactic/expr_to_tactic.h
+++ b/src/library/tactic/expr_to_tactic.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/pos_info_provider.h"
+#include "library/old_type_checker.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/elaborate.h"
 
@@ -27,12 +28,12 @@ bool has_tactic_decls(environment const & env);
 */
 tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p);
 // auxiliary procedure used to compile nested tactic in tacticals
-tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p);
+tactic expr_to_tactic(old_type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p);
 
 name const & get_tactic_name();
 
-unsigned get_unsigned_arg(type_checker & tc, expr const & e, unsigned i);
-optional<unsigned> get_optional_unsigned(type_checker & tc, expr const & e);
+unsigned get_unsigned_arg(old_type_checker & tc, expr const & e, unsigned i);
+optional<unsigned> get_optional_unsigned(old_type_checker & tc, expr const & e);
 
 expr const & get_tactic_expr_type();
 expr const & get_tactic_identifier_type();
@@ -83,7 +84,7 @@ public:
     expr const & get_expr() const { return m_expr; }
 };
 
-typedef std::function<tactic(type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *)>
+typedef std::function<tactic(old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *)>
 expr_to_tactic_fn;
 
 /** \brief Register a new "procedural attachment" for expr_to_tactic. */
diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp
index 777db9327c..267191a8ac 100644
--- a/src/library/tactic/generalize_tactic.cpp
+++ b/src/library/tactic/generalize_tactic.cpp
@@ -93,14 +93,14 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const &
 
 void initialize_generalize_tactic() {
     register_tac(get_tactic_generalize_tac_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(app_fn(e)), "invalid 'generalize' tactic, invalid argument");
                      name id = tactic_expr_to_id(app_arg(e), "invalid 'generalize' tactic, argument must be an identifier");
                      return generalize_tactic(fn, get_tactic_expr_expr(app_arg(app_fn(e))), id);
                  });
 
     register_tac(get_tactic_generalizes_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      buffer<expr> args;
                      get_tactic_expr_list_elements(app_arg(e), args, "invalid 'generalizes' tactic, list of expressions expected");
                      if (args.empty())
diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp
index e79ffa25a0..1fa6ffb4b9 100644
--- a/src/library/tactic/induction_tactic.cpp
+++ b/src/library/tactic/induction_tactic.cpp
@@ -22,7 +22,7 @@ namespace lean {
 class induction_tac {
     environment const &   m_env;
     io_state const &      m_ios;
-    type_checker &        m_tc;
+    old_type_checker &        m_tc;
     name                  m_h_name;
     optional<name>        m_rec_name;
     list<name>            m_ids;
@@ -282,7 +282,7 @@ class induction_tac {
 
 public:
     induction_tac(environment const & env, io_state const & ios,
-                  type_checker & tc, substitution const & subst, name const & h_name,
+                  old_type_checker & tc, substitution const & subst, name const & h_name,
                   optional<name> const & rec_name, list<name> const & ids,
                   bool throw_ex, expr const & ref):
         m_env(env), m_ios(ios), m_tc(tc), m_h_name(h_name), m_rec_name(rec_name), m_ids(ids),
@@ -300,11 +300,11 @@ public:
         if (m_rec_name) {
             recursor_info info      = get_recursor_info(m_env, *m_rec_name);
             name tname              = info.get_type_name();
-            type_checker_ptr aux_tc = mk_type_checker(m_env, [=](name const & n) { return n == tname; });
+            old_type_checker_ptr aux_tc = mk_type_checker(m_env, [=](name const & n) { return n == tname; });
             return aux_tc->whnf(H_type).first;
         } else {
             has_recursors_pred pred(m_env);
-            type_checker_ptr aux_tc = mk_type_checker(m_env, pred);
+            old_type_checker_ptr aux_tc = mk_type_checker(m_env, pred);
             return aux_tc->whnf(H_type).first;
         }
     }
@@ -367,7 +367,7 @@ tactic induction_tactic(name const & H, optional<name> rec, list<name> const & i
         }
         goal  g                          = head(gs);
         goals tail_gs                    = tail(gs);
-        std::unique_ptr<type_checker> tc = mk_type_checker(env);
+        std::unique_ptr<old_type_checker> tc = mk_type_checker(env);
         induction_tac tac(env, ios, *tc, ps.get_subst(), H, rec, ids, ps.report_failure(), ref);
         if (auto res = tac.execute(g)) {
             proof_state new_s(ps, append(*res, tail_gs), tac.get_subst());
@@ -399,7 +399,7 @@ tactic induction_tactic(elaborate_fn const & elab, expr const & H, optional<name
 
 void initialize_induction_tactic() {
     register_tac(name{"tactic", "induction"},
-                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      buffer<expr> args;
                      get_app_args(e, args);
                      if (args.size() != 3)
diff --git a/src/library/tactic/injection_tactic.cpp b/src/library/tactic/injection_tactic.cpp
index 6a5137e599..c24ead3b4e 100644
--- a/src/library/tactic/injection_tactic.cpp
+++ b/src/library/tactic/injection_tactic.cpp
@@ -20,7 +20,7 @@ namespace lean {
 tactic injection_tactic_core(expr const & e, unsigned num, list<name> const & ids, bool report_errors);
 
 // Return true iff lhs and rhs are of the form (f ...) f is a constructor
-bool is_injection_target(type_checker & tc, expr lhs, expr rhs) {
+bool is_injection_target(old_type_checker & tc, expr lhs, expr rhs) {
     environment const & env = tc.env();
     lhs = tc.whnf(lhs).first;
     rhs = tc.whnf(rhs).first;
@@ -232,7 +232,7 @@ tactic injection_tactic(elaborate_fn const & elab, expr const & e, list<name> co
 
 void initialize_injection_tactic() {
     register_tac(name{"tactic", "injection"},
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(app_fn(e)), "invalid 'injection' tactic, invalid argument");
                      buffer<name> ids;
                      get_tactic_id_list_elements(app_arg(e), ids, "invalid 'injection' tactic, list of identifiers expected");
diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp
index 8021ed43fa..22bf2abdcd 100644
--- a/src/library/tactic/intros_tactic.cpp
+++ b/src/library/tactic/intros_tactic.cpp
@@ -74,13 +74,13 @@ tactic intros_tactic(list<name> const & ns) {
 
 void initialize_intros_tactic() {
     register_tac(get_tactic_intro_name(),
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                      buffer<name> ns;
                      get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intro' tactic, arguments must be identifiers");
                      return intro_tactic(to_list(ns.begin(), ns.end()));
                  });
     register_tac(get_tactic_intros_name(),
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                      buffer<name> ns;
                      get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers");
                      return intros_tactic(to_list(ns.begin(), ns.end()));
diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index f6335c9eb3..aa5398c9f5 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -47,7 +47,7 @@ result::result(list<goal> const & gs, list<list<expr>> const & args, list<implem
        b = @eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p :=
     ...
 */
-optional<expr> apply_eq_rec_eq(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & eq_rec) {
+optional<expr> apply_eq_rec_eq(old_type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & eq_rec) {
     buffer<expr> args;
     expr const & eq_rec_fn = get_app_args(eq_rec, args);
     if (args.size() != 6)
@@ -103,7 +103,7 @@ static void replace(implementation_list const & imps, expr const & from, expr co
 class inversion_tac {
     environment const &           m_env;
     io_state const &              m_ios;
-    type_checker &                m_tc;
+    old_type_checker &                m_tc;
     list<name>                    m_ids;
     substitution                  m_subst;
 
@@ -1023,7 +1023,7 @@ class inversion_tac {
 
 public:
     inversion_tac(environment const & env, io_state const & ios,
-                  type_checker & tc, substitution const & subst, list<name> const & ids,
+                  old_type_checker & tc, substitution const & subst, list<name> const & ids,
                   bool throw_tactic_ex, bool clear_elim):
         m_env(env), m_ios(ios), m_tc(tc), m_ids(ids),
         m_subst(subst), m_throw_tactic_exception(throw_tactic_ex),
@@ -1031,7 +1031,7 @@ public:
         m_proof_irrel = m_env.prop_proof_irrel();
     }
 
-    inversion_tac(environment const & env, io_state const & ios, type_checker & tc, bool clear_elim):
+    inversion_tac(environment const & env, io_state const & ios, old_type_checker & tc, bool clear_elim):
         inversion_tac(env, ios, tc, substitution(), list<name>(), false, clear_elim) {}
 
     typedef inversion::result result;
@@ -1086,7 +1086,7 @@ public:
 };
 
 namespace inversion {
-optional<result> apply(environment const & env, io_state const & ios, type_checker & tc,
+optional<result> apply(environment const & env, io_state const & ios, old_type_checker & tc,
                        goal const & g, expr const & h, implementation_list const & imps, bool clear_elim) {
     return inversion_tac(env, ios, tc, clear_elim).execute(g, h, imps);
 }
@@ -1099,7 +1099,7 @@ tactic inversion_tactic(name const & n, list<name> const & ids) {
             return none_proof_state();
         goal  g           = head(gs);
         goals tail_gs     = tail(gs);
-        std::unique_ptr<type_checker> tc = mk_type_checker(env);
+        std::unique_ptr<old_type_checker> tc = mk_type_checker(env);
         bool  clear_elim = true;
         inversion_tac tac(env, ios, *tc, ps.get_subst(), ids, ps.report_failure(), clear_elim);
         if (auto res = tac.execute(g, n, implementation_list())) {
@@ -1129,7 +1129,7 @@ tactic inversion_tactic(elaborate_fn const & elab, expr const & H, list<name> co
 
 void initialize_inversion_tactic() {
     register_tac(get_tactic_cases_name(),
-                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(app_fn(e)), "invalid 'cases' tactic, argument must be an expression");
                      expr H = get_tactic_expr_expr(app_arg(app_fn(e)));
                      buffer<name> ids;
diff --git a/src/library/tactic/inversion_tactic.h b/src/library/tactic/inversion_tactic.h
index 1a086de9eb..7f1a92a59d 100644
--- a/src/library/tactic/inversion_tactic.h
+++ b/src/library/tactic/inversion_tactic.h
@@ -55,7 +55,7 @@ struct result {
            list<rename_map> const & rs, substitution const & subst);
 };
 
-optional<result> apply(environment const & env, io_state const & ios, type_checker & tc,
+optional<result> apply(environment const & env, io_state const & ios, old_type_checker & tc,
                        goal const & g, expr const & h, implementation_list const & imps,
                        bool clear_elim);
 }
diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/tactic/norm_num_tactic.cpp
index b917b59e23..107ade9f3c 100644
--- a/src/library/tactic/norm_num_tactic.cpp
+++ b/src/library/tactic/norm_num_tactic.cpp
@@ -26,7 +26,7 @@ tactic norm_num_tactic() {
                 throw_tactic_exception_if_enabled(s, "norm_num tactic failed, conclusion is not an equality");
                 return none_proof_state();
             }
-            type_checker_ptr rtc = mk_type_checker(env, UnfoldReducible);
+            old_type_checker_ptr rtc = mk_type_checker(env, UnfoldReducible);
             lhs = normalize(*rtc, lhs);
             rhs = normalize(*rtc, rhs);
             buffer<expr> hyps;
@@ -42,7 +42,7 @@ tactic norm_num_tactic() {
                 expr new_rhs_pr = p2.second;
                 mpq v_lhs = mpq_of_expr(ctx, new_lhs), v_rhs = mpq_of_expr(ctx, new_rhs);
                 if (v_lhs == v_rhs) {
-                    type_checker tc(env);
+                    old_type_checker tc(env);
                     expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr));
                     substitution new_subst = s.get_subst();
                     assign(new_subst, g, g_prf);
@@ -60,7 +60,7 @@ tactic norm_num_tactic() {
 
 void initialize_norm_num_tactic() {
     register_tac(name{"tactic", "norm_num"},
-                 [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
                      return norm_num_tactic();
                  });
 }
diff --git a/src/library/tactic/note_tactic.cpp b/src/library/tactic/note_tactic.cpp
index a1f9e0e880..dea5bfb253 100644
--- a/src/library/tactic/note_tactic.cpp
+++ b/src/library/tactic/note_tactic.cpp
@@ -52,7 +52,7 @@ tactic note_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
 
 void initialize_note_tactic() {
     register_tac(get_tactic_note_tac_name(),
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'note' tactic, argument must be an identifier");
                      check_tactic_expr(app_arg(e), "invalid 'note' tactic, argument must be an expression");
                      return note_tactic(fn, id, get_tactic_expr_expr(app_arg(e)));
diff --git a/src/library/tactic/relation_tactics.cpp b/src/library/tactic/relation_tactics.cpp
index 1d4bdc9af2..a07fee6151 100644
--- a/src/library/tactic/relation_tactics.cpp
+++ b/src/library/tactic/relation_tactics.cpp
@@ -82,15 +82,15 @@ tactic trans_tactic(elaborate_fn const & elab, expr const & e) {
 
 void initialize_relation_tactics() {
     register_tac(name{"tactic", "reflexivity"},
-                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
                      return refl_tactic(fn);
                  });
     register_tac(name{"tactic", "symmetry"},
-                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
                      return symm_tactic(fn);
                  });
     register_tac(name{"tactic", "transitivity"},
-                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'transitivity' tactic, invalid argument");
                      return trans_tactic(fn, get_tactic_expr_expr(app_arg(e)));
                  });
diff --git a/src/library/tactic/rename_tactic.cpp b/src/library/tactic/rename_tactic.cpp
index ae3a8eb5da..279370d1f5 100644
--- a/src/library/tactic/rename_tactic.cpp
+++ b/src/library/tactic/rename_tactic.cpp
@@ -50,7 +50,7 @@ static name const & get_rename_arg(expr const & e) {
 }
 
 void initialize_rename_tactic() {
-    auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+    auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
         return rename_tactic(get_rename_arg(app_arg(app_fn(e))),
                              get_rename_arg(app_arg(e)));
     };
diff --git a/src/library/tactic/replace_tactic.cpp b/src/library/tactic/replace_tactic.cpp
index 7adcbb095f..45cfdec031 100644
--- a/src/library/tactic/replace_tactic.cpp
+++ b/src/library/tactic/replace_tactic.cpp
@@ -112,7 +112,7 @@ void initialize_replace_tactic() {
     name replace_tac_name{"tactic", "replace"};
     g_replace_tac          = new expr(Const(replace_tac_name));
     register_tac(replace_tac_name,
-                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      return mk_replace_tactic(elab, e);
                  });
 }
diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp
index e8ae846c1c..741e450528 100644
--- a/src/library/tactic/revert_tactic.cpp
+++ b/src/library/tactic/revert_tactic.cpp
@@ -48,7 +48,7 @@ tactic revert_tactic(name const & n) {
 }
 
 void initialize_revert_tactic() {
-    auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+    auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
         buffer<name> ns;
         get_tactic_id_list_elements(app_arg(e), ns, "invalid 'reverts' tactic, list of identifiers expected");
         tactic r = revert_tactic(ns[0]);
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 63de69d0fb..ae4b0a2c3a 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -16,7 +16,6 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/for_each_fn.h"
-#include "kernel/default_converter.h"
 #include "kernel/inductive/inductive.h"
 #include "library/normalize.h"
 #include "library/kernel_serializer.h"
@@ -475,13 +474,13 @@ class rewrite_match_plugin : public match_plugin {
 #ifdef TRACE_MATCH_PLUGIN
     io_state       m_ios;
 #endif
-    type_checker & m_tc;
+    old_type_checker & m_tc;
 public:
 #ifdef TRACE_MATCH_PLUGIN
-    rewrite_match_plugin(io_state const & ios, type_checker & tc):
+    rewrite_match_plugin(io_state const & ios, old_type_checker & tc):
         m_ios(ios), m_tc(tc) {}
 #else
-    rewrite_match_plugin(io_state const &, type_checker & tc):
+    rewrite_match_plugin(io_state const &, old_type_checker & tc):
         m_tc(tc) {}
 #endif
 
@@ -564,14 +563,13 @@ public:
 };
 
 class rewrite_fn {
-    typedef std::shared_ptr<type_checker> type_checker_ptr;
     environment          m_env;
     io_state             m_ios;
     elaborate_fn         m_elab;
     proof_state          m_ps;
-    type_checker_ptr     m_tc;
-    type_checker_ptr     m_matcher_tc;
-    type_checker_ptr     m_relaxed_tc; // reduce_to and check_trivial
+    old_type_checker_ptr     m_tc;
+    old_type_checker_ptr     m_matcher_tc;
+    old_type_checker_ptr     m_relaxed_tc; // reduce_to and check_trivial
     rewrite_match_plugin m_mplugin;
     goal                 m_g;
     old_local_context    m_ctx;
@@ -647,15 +645,15 @@ class rewrite_fn {
             auto new_e = unfold_rec(m_env, force_unfold, e, to_unfold, *occs);
             if (!new_e)
                 return none_expr();
-            type_checker_ptr tc(new type_checker(m_env,
-                                                 std::unique_ptr<converter>(new rewriter_converter(m_env, list<name>(), unfolded))));
+            old_type_checker_ptr tc(new old_type_checker(m_env,
+                                                         std::unique_ptr<old_converter>(new rewriter_converter(m_env, list<name>(), unfolded))));
             expr r = normalize(*tc, *new_e, cs, use_eta);
             if (cs) // FAIL if generated constraints
                 return none_expr();
             return some_expr(r);
         } else {
-            type_checker_ptr tc(new type_checker(m_env,
-                                                 std::unique_ptr<converter>(new rewriter_converter(m_env, to_unfold, unfolded))));
+            old_type_checker_ptr tc(new old_type_checker(m_env,
+                                                         std::unique_ptr<old_converter>(new rewriter_converter(m_env, to_unfold, unfolded))));
 
             expr r = normalize(*tc, e, cs, use_eta);
             if (!unfolded || cs) // FAIL if didn't unfolded or generated constraints
@@ -1578,7 +1576,7 @@ class rewrite_fn {
         }
     }
 
-    type_checker_ptr mk_matcher_tc(bool full) {
+    old_type_checker_ptr mk_matcher_tc(bool full) {
         if (get_rewriter_syntactic(m_ios.get_options())) {
             // use an everything opaque converter
             return mk_opaque_type_checker(m_env);
@@ -1593,7 +1591,7 @@ class rewrite_fn {
         }
     }
 
-    type_checker_ptr mk_tc(bool full) {
+    old_type_checker_ptr mk_tc(bool full) {
         auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_reducible_pred(m_env);
         return mk_type_checker(m_env, [=](name const & n) {
                 return aux_pred(n) && !is_numeral_const_name(n);
@@ -1772,15 +1770,15 @@ void initialize_rewrite_tactic() {
                                     return mk_macro(def, num, args);
                                 });
     register_tac(rewrite_tac_name,
-                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      return mk_rewrite_tactic(elab, e, false, false);
                  });
     register_tac(name{"tactic", "xrewrite_tac"},
-                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      return mk_rewrite_tactic(elab, e, true, false);
                  });
     register_tac(name{"tactic", "krewrite_tac"},
-                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      return mk_rewrite_tactic(elab, e, true, true);
                  });
 }
diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp
index b242c0b285..6299a74e0b 100644
--- a/src/library/tactic/subst_tactic.cpp
+++ b/src/library/tactic/subst_tactic.cpp
@@ -241,13 +241,13 @@ tactic mk_subst_vars_tactic(bool first, unsigned start) {
 
 void initialize_subst_tactic() {
     register_tac(name{"tactic", "subst"},
-                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      buffer<name> ns;
                      get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected");
                      return then(mk_subst_tactic(to_list(ns)), try_tactic(refl_tactic(elab)));
                  });
     register_tac(name{"tactic", "substvars"},
-                 [](type_checker &, elaborate_fn const & elab, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const & elab, expr const &, pos_info_provider const *) {
                      return then(mk_subst_vars_tactic(true, 0), try_tactic(refl_tactic(elab)));
                  });
 }
diff --git a/src/library/tactic/trace_tactic.cpp b/src/library/tactic/trace_tactic.cpp
index 6bb03a51b9..2cae51041e 100644
--- a/src/library/tactic/trace_tactic.cpp
+++ b/src/library/tactic/trace_tactic.cpp
@@ -62,7 +62,7 @@ tactic suppress_trace(tactic const & t) {
 
 void initialize_trace_tactic() {
     register_tac(get_tactic_state_name(),
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) {
+                 [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) {
                      if (p)
                          if (auto it = p->get_pos_info(e))
                              return trace_state_tactic(std::string(p->get_file_name()), *it);
@@ -70,7 +70,7 @@ void initialize_trace_tactic() {
                  });
 
     register_tac(get_tactic_trace_name(),
-                 [](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                 [](old_type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                      buffer<expr> args;
                      get_app_args(e, args);
                      if (args.size() != 1)
diff --git a/src/library/tactic/unfold_rec.cpp b/src/library/tactic/unfold_rec.cpp
index bb298175ac..8948cd0eb4 100644
--- a/src/library/tactic/unfold_rec.cpp
+++ b/src/library/tactic/unfold_rec.cpp
@@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/fresh_name.h"
-#include "kernel/type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive/inductive.h"
 #include "library/util.h"
+#include "library/old_type_checker.h"
 #include "library/replace_visitor.h"
 #include "library/constants.h"
 #include "library/user_recursors.h"
@@ -47,8 +47,8 @@ protected:
 class unfold_rec_fn : public replace_visitor_aux {
     environment const & m_env;
     bool                m_force_unfold;
-    type_checker_ptr    m_tc;
-    type_checker_ptr    m_norm_decl_tc;
+    old_type_checker_ptr    m_tc;
+    old_type_checker_ptr    m_norm_decl_tc;
     list<name>          m_to_unfold;
     occurrence          m_occs;
     unsigned            m_occ_idx;
@@ -191,7 +191,7 @@ class unfold_rec_fn : public replace_visitor_aux {
     struct fold_failed {};
 
     struct fold_rec_fn : public replace_visitor_aux {
-        type_checker_ptr &       m_tc;
+        old_type_checker_ptr &       m_tc;
         expr                     m_fn;    // function being unfolded
         buffer<expr> const &     m_args;  // arguments of the function being unfolded
         rec_kind                 m_kind;
@@ -202,7 +202,7 @@ class unfold_rec_fn : public replace_visitor_aux {
         buffer<unsigned> const & m_rec_arg_pos; // position of the other arguments that are not fixed in the recursion
         name                     m_prod_rec_name;
 
-        fold_rec_fn(type_checker_ptr & tc, expr const & fn, buffer<expr> const & args, rec_kind k, name const & rec_name,
+        fold_rec_fn(old_type_checker_ptr & tc, expr const & fn, buffer<expr> const & args, rec_kind k, name const & rec_name,
                     buffer<unsigned> const & indices_pos, unsigned main_pos, buffer<unsigned> const & rec_arg_pos):
             m_tc(tc), m_fn(fn), m_args(args), m_kind(k), m_rec_name(rec_name),
             m_major_idx(*inductive::get_elim_major_idx(m_tc->env(), rec_name)),
diff --git a/src/library/tactic/whnf_tactic.cpp b/src/library/tactic/whnf_tactic.cpp
index d5bc87fb95..23a140b00d 100644
--- a/src/library/tactic/whnf_tactic.cpp
+++ b/src/library/tactic/whnf_tactic.cpp
@@ -33,7 +33,7 @@ tactic whnf_tactic() {
 
 void initialize_whnf_tactic() {
     register_tac(get_tactic_whnf_name(),
-                 [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
+                 [](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
                      return whnf_tactic();
                  });
 }
diff --git a/src/library/tactic/with_options_tactic.cpp b/src/library/tactic/with_options_tactic.cpp
index 4e128d3b08..874c17db83 100644
--- a/src/library/tactic/with_options_tactic.cpp
+++ b/src/library/tactic/with_options_tactic.cpp
@@ -81,7 +81,7 @@ void initialize_with_options_tactic() {
     name with_options_tac_name{"tactic", "with_options_tac"};
     g_with_options_tac = new expr(Const(with_options_tac_name));
     register_tac(with_options_tac_name,
-                 [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
+                 [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
                      buffer<expr> args;
                      get_app_args(e, args);
                      if (args.size() != 2)
diff --git a/src/library/tc_multigraph.cpp b/src/library/tc_multigraph.cpp
index dec4000552..7329e74011 100644
--- a/src/library/tc_multigraph.cpp
+++ b/src/library/tc_multigraph.cpp
@@ -5,19 +5,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/sstream.h"
-#include "kernel/type_checker.h"
 #include "library/tc_multigraph.h"
+#include "library/old_type_checker.h"
 #include "library/composition_manager.h"
 #include "library/util.h"
 
 namespace lean {
 struct add_edge_fn {
     environment      m_env;
-    type_checker_ptr m_tc;
+    old_type_checker_ptr m_tc;
     tc_multigraph &  m_graph;
 
     add_edge_fn(environment const & env, tc_multigraph & g):
-        m_env(env), m_tc(new type_checker(env)), m_graph(g) {}
+        m_env(env), m_tc(new old_type_checker(env)), m_graph(g) {}
 
     // Return true iff the types of constants c1 and c2 are equal.
     bool is_def_eq(name const & c1, name const & c2) {
@@ -82,7 +82,7 @@ struct add_edge_fn {
                 }
             }
         }
-        m_tc.reset(new type_checker(m_env)); // update to reflect new constants in the environment
+        m_tc.reset(new old_type_checker(m_env)); // update to reflect new constants in the environment
         buffer<tc_edge> new_back_edges;
         new_back_edges.append(new_edges);
         if (auto succs = m_graph.m_successors.find(tgt)) {
diff --git a/src/library/type_util.cpp b/src/library/type_util.cpp
index 852c2e9ffe..acec41a35d 100644
--- a/src/library/type_util.cpp
+++ b/src/library/type_util.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "library/type_util.h"
 
 namespace lean {
-unsigned get_expect_num_args(type_checker & tc, expr e) {
+unsigned get_expect_num_args(old_type_checker & tc, expr e) {
     unsigned r = 0;
     while (true) {
         e = tc.whnf(e).first;
diff --git a/src/library/type_util.h b/src/library/type_util.h
index 1d72acd549..c20eb8a56b 100644
--- a/src/library/type_util.h
+++ b/src/library/type_util.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "kernel/type_checker.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 /** \brief Given an expression \c e, return the number of arguments expected arguments.
@@ -14,5 +14,5 @@ namespace lean {
     Pi's. Weak-head-normal-forms are computed for the type of \c e.
     \remark The type and whnf are computed using \c tc.
 */
-unsigned get_expect_num_args(type_checker & tc, expr e);
+unsigned get_expect_num_args(old_type_checker & tc, expr e);
 }
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index ce121fe44d..611cbf31cb 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -19,7 +19,6 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/error_msgs.h"
 #include "library/trace.h"
@@ -34,6 +33,7 @@ Author: Leonardo de Moura
 #include "library/expr_lt.h"
 #include "library/projection.h"
 #include "library/coercion.h"
+#include "library/old_type_checker.h"
 
 #ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS
 #define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000
@@ -338,7 +338,7 @@ struct unifier_fn {
     typedef name_map<cnstr_idx_set> name_to_cnstrs;
     typedef name_map<unsigned> owned_map;
     typedef rb_map<expr, pair<expr, justification>, expr_quick_cmp> expr_map;
-    typedef std::shared_ptr<type_checker> type_checker_ptr;
+    typedef std::shared_ptr<old_type_checker> type_checker_ptr;
     environment      m_env;
     substitution     m_subst;
     constraints      m_postponed; // constraints that will not be solved
@@ -1795,11 +1795,11 @@ struct unifier_fn {
         bool cheap() const { return u.m_config.m_kind == unifier_kind::Cheap; }
         bool pattern() const { return u.m_config.m_pattern; }
 
-        type_checker & tc() {
+        old_type_checker & tc() {
             return *u.m_tc;
         }
 
-        type_checker & restricted_tc() {
+        old_type_checker & restricted_tc() {
             return *u.m_flex_rigid_tc;
         }
 
diff --git a/src/library/unifier_plugin.cpp b/src/library/unifier_plugin.cpp
index 7b76d44a24..fd15ce1047 100644
--- a/src/library/unifier_plugin.cpp
+++ b/src/library/unifier_plugin.cpp
@@ -14,7 +14,7 @@ protected:
     unifier_plugin m_p2;
 public:
     binary_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):m_p1(p1), m_p2(p2) {}
-    virtual bool delay_constraint(type_checker & tc, constraint const & c) const {
+    virtual bool delay_constraint(old_type_checker & tc, constraint const & c) const {
         return m_p1->delay_constraint(tc, c) || m_p2->delay_constraint(tc, c);
     }
 };
@@ -22,7 +22,7 @@ public:
 class append_unifier_plugin_cell : public binary_unifier_plugin_cell {
 public:
     append_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
-    virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c) const {
+    virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
         return append(m_p1->solve(tc, c), m_p2->solve(tc, c));
     }
 };
@@ -30,7 +30,7 @@ public:
 class orelse_unifier_plugin_cell : public binary_unifier_plugin_cell {
 public:
     orelse_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
-    virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c) const {
+    virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
         return orelse(m_p1->solve(tc, c), m_p2->solve(tc, c));
     }
 };
@@ -46,10 +46,10 @@ unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2) {
 static unifier_plugin noop_unifier_plugin() {
     class noop_unifier_plugin_cell : public unifier_plugin_cell {
     public:
-        virtual lazy_list<constraints> solve(type_checker &, constraint const &) const {
+        virtual lazy_list<constraints> solve(old_type_checker &, constraint const &) const {
             return lazy_list<constraints>();
         }
-        virtual bool delay_constraint(type_checker &, constraint const &) const { return false; }
+        virtual bool delay_constraint(old_type_checker &, constraint const &) const { return false; }
     };
     return std::make_shared<noop_unifier_plugin_cell>();
 }
diff --git a/src/library/unifier_plugin.h b/src/library/unifier_plugin.h
index 5e64c88299..04c87ca1b9 100644
--- a/src/library/unifier_plugin.h
+++ b/src/library/unifier_plugin.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/lazy_list.h"
 #include "kernel/environment.h"
 #include "kernel/constraint.h"
-#include "kernel/type_checker.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 /**
@@ -23,8 +23,8 @@ namespace lean {
 class unifier_plugin_cell {
 public:
     virtual ~unifier_plugin_cell() {}
-    virtual lazy_list<constraints> solve(type_checker &, constraint const &) const = 0;
-    virtual bool delay_constraint(type_checker &, constraint const &) const = 0;
+    virtual lazy_list<constraints> solve(old_type_checker &, constraint const &) const = 0;
+    virtual bool delay_constraint(old_type_checker &, constraint const &) const = 0;
 };
 
 typedef std::shared_ptr<unifier_plugin_cell> unifier_plugin;
diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index ead18b1125..4ca4d8412a 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -94,7 +94,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
                              num_args, major_pos, params_pos, indices_pos, produce_motive);
     }
     declaration d = env.get(r);
-    type_checker tc(env);
+    old_type_checker tc(env);
     buffer<expr> tele;
     expr rtype    = to_telescope(tc, d.get_type(), tele);
     buffer<expr> C_args;
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 1acccfb06f..88f8acf399 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/error_msgs.h"
 #include "kernel/abstract.h"
-#include "kernel/type_checker.h"
 #include "kernel/default_converter.h"
 #include "kernel/metavar.h"
 #include "kernel/inductive/inductive.h"
@@ -19,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/unfold_macros.h"
 #include "library/pp_options.h"
 #include "library/projection.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 bool is_app_of(expr const & t, name const & f_name) {
@@ -35,7 +35,7 @@ bool is_standard(environment const & env) {
     return env.prop_proof_irrel() && env.impredicative();
 }
 
-bool is_norm_pi(type_checker & tc, expr & e, constraint_seq & cs) {
+bool is_norm_pi(old_type_checker & tc, expr & e, constraint_seq & cs) {
     constraint_seq new_cs = cs;
     expr new_e = tc.whnf(e, new_cs);
     if (is_pi(new_e)) {
@@ -161,7 +161,7 @@ bool is_recursive_datatype(environment const & env, name const & n) {
     return false;
 }
 
-bool is_reflexive_datatype(type_checker & tc, name const & n) {
+bool is_reflexive_datatype(old_type_checker & tc, name const & n) {
     environment const & env = tc.env();
     optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
     if (!decls)
@@ -258,7 +258,7 @@ expr fun_to_telescope(expr const & e, buffer<expr> & telescope,
     return to_telescope(false, e, telescope, binfo);
 }
 
-expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo,
+expr to_telescope(old_type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo,
                   constraint_seq & cs) {
     expr new_type = tc.whnf(type, cs);
     while (is_pi(new_type)) {
@@ -275,7 +275,7 @@ expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, option
     return type;
 }
 
-expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
+expr to_telescope(old_type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
     constraint_seq cs;
     return to_telescope(tc, type, telescope, binfo, cs);
 }
@@ -304,7 +304,7 @@ bool is_false(environment const & env, expr const & e) {
     return is_standard(env) ? is_false(e) : is_empty(e);
 }
 
-expr mk_false_rec(type_checker & tc, expr const & f, expr const & t) {
+expr mk_false_rec(old_type_checker & tc, expr const & f, expr const & t) {
     level t_lvl = sort_level(tc.ensure_type(t).first);
     if (is_standard(tc.env())) {
         return mk_app(mk_constant(get_false_rec_name(), {t_lvl}), t, f);
@@ -364,7 +364,7 @@ bool is_not(environment const & env, expr const & e) {
     }
 }
 
-expr mk_not(type_checker & tc, expr const & e) {
+expr mk_not(old_type_checker & tc, expr const & e) {
     if (is_standard(tc.env())) {
         return mk_app(mk_constant(get_not_name()), e);
     } else {
@@ -373,7 +373,7 @@ expr mk_not(type_checker & tc, expr const & e) {
     }
 }
 
-expr mk_absurd(type_checker & tc, expr const & t, expr const & e, expr const & not_e) {
+expr mk_absurd(old_type_checker & tc, expr const & t, expr const & e, expr const & not_e) {
     level t_lvl  = sort_level(tc.ensure_type(t).first);
     expr  e_type = tc.infer(e).first;
     if (is_standard(tc.env())) {
@@ -384,7 +384,7 @@ expr mk_absurd(type_checker & tc, expr const & t, expr const & e, expr const & n
     }
 }
 
-optional<expr> lift_down_if_hott(type_checker & tc, expr const & v) {
+optional<expr> lift_down_if_hott(old_type_checker & tc, expr const & v) {
     if (is_standard(tc.env())) {
         return some_expr(v);
     } else {
@@ -464,16 +464,16 @@ expr mk_and(expr const & a, expr const & b) {
     return mk_app(*g_and, a, b);
 }
 
-expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb) {
+expr mk_and_intro(old_type_checker & tc, expr const & Ha, expr const & Hb) {
     return mk_app(*g_and_intro, tc.infer(Ha).first, tc.infer(Hb).first, Ha, Hb);
 }
 
-expr mk_and_elim_left(type_checker & tc, expr const & H) {
+expr mk_and_elim_left(old_type_checker & tc, expr const & H) {
     expr a_and_b = tc.whnf(tc.infer(H).first).first;
     return mk_app(*g_and_elim_left, app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
 }
 
-expr mk_and_elim_right(type_checker & tc, expr const & H) {
+expr mk_and_elim_right(old_type_checker & tc, expr const & H) {
     expr a_and_b = tc.whnf(tc.infer(H).first).first;
     return mk_app(*g_and_elim_right, app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
 }
@@ -486,13 +486,13 @@ expr mk_unit_mk(level const & l) {
     return mk_constant(get_poly_unit_star_name(), {l});
 }
 
-expr mk_prod(type_checker & tc, expr const & A, expr const & B) {
+expr mk_prod(old_type_checker & tc, expr const & A, expr const & B) {
     level l1 = sort_level(tc.ensure_type(A).first);
     level l2 = sort_level(tc.ensure_type(B).first);
     return mk_app(mk_constant(get_prod_name(), {l1, l2}), A, B);
 }
 
-expr mk_pair(type_checker & tc, expr const & a, expr const & b) {
+expr mk_pair(old_type_checker & tc, expr const & a, expr const & b) {
     expr A = tc.infer(a).first;
     expr B = tc.infer(b).first;
     level l1 = sort_level(tc.ensure_type(A).first);
@@ -500,14 +500,14 @@ expr mk_pair(type_checker & tc, expr const & a, expr const & b) {
     return mk_app(mk_constant(get_prod_mk_name(), {l1, l2}), A, B, a, b);
 }
 
-expr mk_pr1(type_checker & tc, expr const & p) {
+expr mk_pr1(old_type_checker & tc, expr const & p) {
     expr AxB = tc.whnf(tc.infer(p).first).first;
     expr const & A = app_arg(app_fn(AxB));
     expr const & B = app_arg(AxB);
     return mk_app(mk_constant(get_prod_pr1_name(), const_levels(get_app_fn(AxB))), A, B, p);
 }
 
-expr mk_pr2(type_checker & tc, expr const & p) {
+expr mk_pr2(old_type_checker & tc, expr const & p) {
     expr AxB = tc.whnf(tc.infer(p).first).first;
     expr const & A = app_arg(app_fn(AxB));
     expr const & B = app_arg(AxB);
@@ -516,12 +516,12 @@ expr mk_pr2(type_checker & tc, expr const & p) {
 
 expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); }
 expr mk_unit_mk(level const & l, bool prop) { return prop ? mk_true_intro() : mk_unit_mk(l); }
-expr mk_prod(type_checker & tc, expr const & a, expr const & b, bool prop) { return prop ? mk_and(a, b) : mk_prod(tc, a, b); }
-expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop) {
+expr mk_prod(old_type_checker & tc, expr const & a, expr const & b, bool prop) { return prop ? mk_and(a, b) : mk_prod(tc, a, b); }
+expr mk_pair(old_type_checker & tc, expr const & a, expr const & b, bool prop) {
     return prop ? mk_and_intro(tc, a, b) : mk_pair(tc, a, b);
 }
-expr mk_pr1(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_left(tc, p) : mk_pr1(tc, p); }
-expr mk_pr2(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_right(tc, p) : mk_pr2(tc, p); }
+expr mk_pr1(old_type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_left(tc, p) : mk_pr1(tc, p); }
+expr mk_pr2(old_type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_right(tc, p) : mk_pr2(tc, p); }
 
 bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f) {
     expr const & fn = get_app_fn(e);
@@ -573,19 +573,19 @@ expr apply_propext(expr const & iff_pr, expr const & iff_term) {
     return mk_app(mk_constant(get_propext_name()), app_arg(app_fn(iff_term)), app_arg(iff_term), iff_pr);
 }
 
-expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) {
+expr mk_eq(old_type_checker & tc, expr const & lhs, expr const & rhs) {
     expr A    = tc.whnf(tc.infer(lhs).first).first;
     level lvl = sort_level(tc.ensure_type(A).first);
     return mk_app(mk_constant(get_eq_name(), {lvl}), A, lhs, rhs);
 }
 
-expr mk_refl(type_checker & tc, expr const & a) {
+expr mk_refl(old_type_checker & tc, expr const & a) {
     expr A    = tc.whnf(tc.infer(a).first).first;
     level lvl = sort_level(tc.ensure_type(A).first);
     return mk_app(mk_constant(get_eq_refl_name(), {lvl}), A, a);
 }
 
-expr mk_symm(type_checker & tc, expr const & H) {
+expr mk_symm(old_type_checker & tc, expr const & H) {
     expr p    = tc.whnf(tc.infer(H).first).first;
     lean_assert(is_eq(p));
     expr lhs  = app_arg(app_fn(p));
@@ -595,7 +595,7 @@ expr mk_symm(type_checker & tc, expr const & H) {
     return mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H);
 }
 
-expr mk_trans(type_checker & tc, expr const & H1, expr const & H2) {
+expr mk_trans(old_type_checker & tc, expr const & H1, expr const & H2) {
     expr p1    = tc.whnf(tc.infer(H1).first).first;
     expr p2    = tc.whnf(tc.infer(H2).first).first;
     lean_assert(is_eq(p1) && is_eq(p2));
@@ -607,7 +607,7 @@ expr mk_trans(type_checker & tc, expr const & H1, expr const & H2) {
     return mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, lhs1, rhs1, rhs2, H1, H2});
 }
 
-expr mk_subst(type_checker & tc, expr const & motive, expr const & x, expr const & y, expr const & xeqy, expr const & h) {
+expr mk_subst(old_type_checker & tc, expr const & motive, expr const & x, expr const & y, expr const & xeqy, expr const & h) {
     expr A    = tc.infer(x).first;
     level l1  = sort_level(tc.ensure_type(A).first);
     expr r;
@@ -620,12 +620,12 @@ expr mk_subst(type_checker & tc, expr const & motive, expr const & x, expr const
     return mk_app({r, A, x, y, motive, xeqy, h});
 }
 
-expr mk_subst(type_checker & tc, expr const & motive, expr const & xeqy, expr const & h) {
+expr mk_subst(old_type_checker & tc, expr const & motive, expr const & xeqy, expr const & h) {
     expr xeqy_type = tc.whnf(tc.infer(xeqy).first).first;
     return mk_subst(tc, motive, app_arg(app_fn(xeqy_type)), app_arg(xeqy_type), xeqy, h);
 }
 
-expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, expr const & y) {
+expr mk_subsingleton_elim(old_type_checker & tc, expr const & h, expr const & x, expr const & y) {
     expr A  = tc.infer(x).first;
     level l = sort_level(tc.ensure_type(A).first);
     expr r;
@@ -637,7 +637,7 @@ expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, exp
     return mk_app({r, A, h, x, y});
 }
 
-expr mk_heq(type_checker & tc, expr const & lhs, expr const & rhs) {
+expr mk_heq(old_type_checker & tc, expr const & lhs, expr const & rhs) {
     expr A    = tc.whnf(tc.infer(lhs).first).first;
     expr B    = tc.whnf(tc.infer(rhs).first).first;
     level lvl = sort_level(tc.ensure_type(A).first);
@@ -693,7 +693,7 @@ bool is_eq_a_a(expr const & e) {
     return args.size() == 3 && args[1] == args[2];
 }
 
-bool is_eq_a_a(type_checker & tc, expr const & e) {
+bool is_eq_a_a(old_type_checker & tc, expr const & e) {
     if (!is_eq(e))
         return false;
     buffer<expr> args;
@@ -722,7 +722,7 @@ bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs) {
     }
 }
 
-void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs) {
+void mk_telescopic_eq(old_type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs) {
     lean_assert(t.size() == s.size());
     lean_assert(std::all_of(s.begin(), s.end(), is_local));
     lean_assert(inductive::has_dep_elim(tc.env(), get_eq_name()));
@@ -763,7 +763,7 @@ void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> co
     }
 }
 
-void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> & eqs) {
+void mk_telescopic_eq(old_type_checker & tc, buffer<expr> const & t, buffer<expr> & eqs) {
     lean_assert(std::all_of(t.begin(), t.end(), is_local));
     lean_assert(inductive::has_dep_elim(tc.env(), get_eq_name()));
     buffer<expr> s;
@@ -786,7 +786,7 @@ level mk_max(levels const & ls) {
         return mk_max(head(ls), mk_max(tail(ls)));
 }
 
-expr telescope_to_sigma(type_checker & tc, unsigned sz, expr const * ts, constraint_seq & cs) {
+expr telescope_to_sigma(old_type_checker & tc, unsigned sz, expr const * ts, constraint_seq & cs) {
     lean_assert(sz > 0);
     unsigned i = sz - 1;
     expr r = mlocal_type(ts[i]);
@@ -802,7 +802,7 @@ expr telescope_to_sigma(type_checker & tc, unsigned sz, expr const * ts, constra
     return r;
 }
 
-expr mk_sigma_mk(type_checker & tc, unsigned sz, expr const * ts, expr const * as, constraint_seq & cs) {
+expr mk_sigma_mk(old_type_checker & tc, unsigned sz, expr const * ts, expr const * as, constraint_seq & cs) {
     lean_assert(sz > 0);
     if (sz == 1)
         return as[0];
@@ -819,7 +819,7 @@ expr mk_sigma_mk(type_checker & tc, unsigned sz, expr const * ts, expr const * a
     return mk_app(mk_constant(get_sigma_mk_name(), {l1, l2}), arg1, arg2, arg3, arg4);
 }
 
-expr mk_sigma_mk(type_checker & tc, buffer<expr> const & ts, buffer<expr> const & as, constraint_seq & cs) {
+expr mk_sigma_mk(old_type_checker & tc, buffer<expr> const & ts, buffer<expr> const & as, constraint_seq & cs) {
     lean_assert(ts.size() == as.size());
     return mk_sigma_mk(tc, ts.size(), ts.data(), as.data(), cs);
 }
@@ -905,14 +905,14 @@ constraint instantiate_metavars(constraint const & c, substitution & s) {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-void check_term(type_checker & tc, expr const & e) {
+void check_term(old_type_checker & tc, expr const & e) {
     expr tmp = unfold_untrusted_macros(tc.env(), e);
     tc.check_ignore_undefined_universes(tmp);
 }
 
 void check_term(environment const & env, expr const & e) {
     expr tmp = unfold_untrusted_macros(env, e);
-    type_checker(env).check_ignore_undefined_universes(tmp);
+    old_type_checker(env).check_ignore_undefined_universes(tmp);
 }
 
 format pp_type_mismatch(formatter const & fmt, expr const & v, expr const & v_type, expr const & t) {
@@ -1006,21 +1006,21 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
     return mk_justification(m, [=](formatter const & fmt, substitution const & subst, bool) {
             substitution tmp(subst);
             expr new_m    = instantiate_meta(m, tmp);
-            expr new_type = type_checker(env).infer(new_m).first;
+            expr new_type = old_type_checker(env).infer(new_m).first;
             buffer<expr> hyps;
             get_app_args(new_m, hyps);
             return format("failed to synthesize placeholder") + line() + format_goal(fmt, hyps, new_type, subst);
         });
 }
 
-type_checker_ptr mk_type_checker(environment const & env, name_predicate const & pred) {
-    return std::unique_ptr<type_checker>(new type_checker(env,
-                                                          std::unique_ptr<converter>(new hint_converter<projection_converter>(env, pred))));
+old_type_checker_ptr mk_type_checker(environment const & env, name_predicate const & pred) {
+    return std::unique_ptr<old_type_checker>(new old_type_checker(env,
+                                                          std::unique_ptr<old_converter>(new hint_old_converter<projection_converter>(env, pred))));
 }
 
-type_checker_ptr mk_simple_type_checker(environment const & env, name_predicate const & pred) {
-    return std::unique_ptr<type_checker>(new type_checker(env,
-                                                          std::unique_ptr<converter>(new hint_converter<default_converter>(env, pred))));
+old_type_checker_ptr mk_simple_type_checker(environment const & env, name_predicate const & pred) {
+    return std::unique_ptr<old_type_checker>(new old_type_checker(env,
+                                                          std::unique_ptr<old_converter>(new hint_old_converter<old_default_converter>(env, pred))));
 }
 
 bool is_internal_name(name const & n) {
diff --git a/src/library/util.h b/src/library/util.h
index 85ec1b2b7c..3fdc0f5a86 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
-#include "kernel/type_checker.h"
+#include "library/old_type_checker.h"
 
 namespace lean {
 /** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
@@ -14,7 +14,7 @@ bool is_app_of(expr const & t, name const & f_name);
 /** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_nargs) */
 bool is_app_of(expr const & t, name const & f_name, unsigned nargs);
 
-typedef std::unique_ptr<type_checker> type_checker_ptr;
+typedef std::unique_ptr<old_type_checker> old_type_checker_ptr;
 /** \brief Unfold constant \c e or constant application (i.e., \c e is of the form (f ....),
     where \c f is a constant */
 optional<expr> unfold_term(environment const & env, expr const & e);
@@ -58,7 +58,7 @@ bool is_recursive_datatype(environment const & env, name const & n);
     We say an inductive type T is reflexive if it contains at least one constructor that
     takes as an argument a function returning T.
 */
-bool is_reflexive_datatype(type_checker & tc, name const & n);
+bool is_reflexive_datatype(old_type_checker & tc, name const & n);
 
 /** \brief Return true iff \c n is an inductive predicate, i.e., an inductive datatype that is in Prop.
 
@@ -90,14 +90,14 @@ optional<name> is_constructor_app_ext(environment const & env, expr const & e);
 expr to_telescope(expr const & type, buffer<expr> & telescope,
                   optional<binder_info> const & binfo = optional<binder_info>());
 /** \brief Similar to previous procedure, but puts \c type in whnf */
-expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope,
+expr to_telescope(old_type_checker & tc, expr type, buffer<expr> & telescope,
                   optional<binder_info> const & binfo = optional<binder_info>());
 /** \brief Similar to previous procedure, but also accumulates constraints generated while
     normalizing type.
 
     \remark Constraints are generated only if \c type constains metavariables.
 */
-expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo,
+expr to_telescope(old_type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo,
                   constraint_seq & cs);
 
 /** \brief "Consume" fun/lambda. This procedure creates local constants based on the arguments of \c e
@@ -122,23 +122,23 @@ bool is_and(expr const & e, expr & arg1, expr & arg2);
 bool is_and(expr const & e);
 
 expr mk_and(expr const & a, expr const & b);
-expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb);
-expr mk_and_elim_left(type_checker & tc, expr const & H);
-expr mk_and_elim_right(type_checker & tc, expr const & H);
+expr mk_and_intro(old_type_checker & tc, expr const & Ha, expr const & Hb);
+expr mk_and_elim_left(old_type_checker & tc, expr const & H);
+expr mk_and_elim_right(old_type_checker & tc, expr const & H);
 
 expr mk_poly_unit(level const & l);
 expr mk_poly_unit_mk(level const & l);
-expr mk_prod(type_checker & tc, expr const & A, expr const & B);
-expr mk_pair(type_checker & tc, expr const & a, expr const & b);
-expr mk_pr1(type_checker & tc, expr const & p);
-expr mk_pr2(type_checker & tc, expr const & p);
+expr mk_prod(old_type_checker & tc, expr const & A, expr const & B);
+expr mk_pair(old_type_checker & tc, expr const & a, expr const & b);
+expr mk_pr1(old_type_checker & tc, expr const & p);
+expr mk_pr2(old_type_checker & tc, expr const & p);
 
 expr mk_unit(level const & l, bool prop);
 expr mk_unit_mk(level const & l, bool prop);
-expr mk_prod(type_checker & tc, expr const & a, expr const & b, bool prop);
-expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop);
-expr mk_pr1(type_checker & tc, expr const & p, bool prop);
-expr mk_pr2(type_checker & tc, expr const & p, bool prop);
+expr mk_prod(old_type_checker & tc, expr const & a, expr const & b, bool prop);
+expr mk_pair(old_type_checker & tc, expr const & a, expr const & b, bool prop);
+expr mk_pr1(old_type_checker & tc, expr const & p, bool prop);
+expr mk_pr2(old_type_checker & tc, expr const & p, bool prop);
 
 expr mk_false();
 expr mk_empty();
@@ -150,7 +150,7 @@ bool is_empty(expr const & e);
 /** \brief Return true iff \c e is false (in standard mode) or empty (in HoTT) mode */
 bool is_false(environment const & env, expr const & e);
 /** \brief Return an element of type t given an element \c f : false (in standard mode) and empty (in HoTT) mode */
-expr mk_false_rec(type_checker & tc, expr const & f, expr const & t);
+expr mk_false_rec(old_type_checker & tc, expr const & f, expr const & t);
 
 bool is_or(expr const & e);
 bool is_or(expr const & e, expr & A, expr & B);
@@ -159,19 +159,19 @@ bool is_or(expr const & e, expr & A, expr & B);
      Return false otherwise */
 bool is_not(environment const & env, expr const & e, expr & a);
 bool is_not(environment const & env, expr const & e);
-expr mk_not(type_checker & tc, expr const & e);
+expr mk_not(old_type_checker & tc, expr const & e);
 
 /** \brief Create the term <tt>absurd e not_e : t</tt>. */
-expr mk_absurd(type_checker & tc, expr const & t, expr const & e, expr const & not_e);
+expr mk_absurd(old_type_checker & tc, expr const & t, expr const & e, expr const & not_e);
 
-expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs);
-expr mk_refl(type_checker & tc, expr const & a);
-expr mk_symm(type_checker & tc, expr const & H);
-expr mk_trans(type_checker & tc, expr const & H1, expr const & H2);
-expr mk_subst(type_checker & tc, expr const & motive, expr const & x, expr const & y, expr const & xeqy, expr const & h);
-expr mk_subst(type_checker & tc, expr const & motive, expr const & xeqy, expr const & h);
+expr mk_eq(old_type_checker & tc, expr const & lhs, expr const & rhs);
+expr mk_refl(old_type_checker & tc, expr const & a);
+expr mk_symm(old_type_checker & tc, expr const & H);
+expr mk_trans(old_type_checker & tc, expr const & H1, expr const & H2);
+expr mk_subst(old_type_checker & tc, expr const & motive, expr const & x, expr const & y, expr const & xeqy, expr const & h);
+expr mk_subst(old_type_checker & tc, expr const & motive, expr const & xeqy, expr const & h);
 /** \brief Create an proof for x = y using subsingleton.elim (in standard mode) and is_trunc.is_prop.elim (in HoTT mode) */
-expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, expr const & y);
+expr mk_subsingleton_elim(old_type_checker & tc, expr const & h, expr const & x, expr const & y);
 
 /** \brief Return true iff \c e is a term of the form (eq.rec ....) */
 bool is_eq_rec_core(expr const & e);
@@ -188,7 +188,7 @@ bool is_eq(expr const & e, expr & A, expr & lhs, expr & rhs);
 /** \brief Return true iff \c e is of the form (eq A a a) */
 bool is_eq_a_a(expr const & e);
 /** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */
-bool is_eq_a_a(type_checker & tc, expr const & e);
+bool is_eq_a_a(old_type_checker & tc, expr const & e);
 
 bool is_heq(expr const & e);
 bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs);
@@ -209,18 +209,18 @@ expr apply_propext(expr const & iff_pr, expr const & iff_term);
     The no_confusion constructions uses lifts in the proof relevant version (aka HoTT mode).
     We must apply lift.down to eliminate the auxiliary lift.
 */
-optional<expr> lift_down_if_hott(type_checker & tc, expr const & v);
+optional<expr> lift_down_if_hott(old_type_checker & tc, expr const & v);
 
 /** \brief Create a telescope equality for HoTT library.
     This procedure assumes eq supports dependent elimination.
     For HoTT, we can't use heterogeneous equality.
 */
-void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs);
-void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> & eqs);
+void mk_telescopic_eq(old_type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs);
+void mk_telescopic_eq(old_type_checker & tc, buffer<expr> const & t, buffer<expr> & eqs);
 
 level mk_max(levels const & ls);
 
-expr mk_sigma_mk(type_checker & tc, buffer<expr> const & ts, buffer<expr> const & as, constraint_seq & cs);
+expr mk_sigma_mk(old_type_checker & tc, buffer<expr> const & ts, buffer<expr> const & as, constraint_seq & cs);
 
 /** \brief Return true iff \c e is of the form (@option.none A), and update \c A */
 bool is_none(expr const & e, expr & A);
@@ -252,7 +252,7 @@ constraint instantiate_metavars(constraint const & c, substitution & s);
     These procedures are useful for checking whether intermediate results produced by
     tactics and automation are type correct.
 */
-void check_term(type_checker & tc, expr const & e);
+void check_term(old_type_checker & tc, expr const & e);
 void check_term(environment const & env, expr const & e);
 
 /** \brief Return a justification for \c v_type being definitionally equal to \c t,
@@ -266,10 +266,10 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e
 
 /** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true.
     Projections are reduced using the projection converter */
-type_checker_ptr mk_type_checker(environment const & env, name_predicate const & pred);
+old_type_checker_ptr mk_type_checker(environment const & env, name_predicate const & pred);
 /** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true.
     No special support for projections is used */
-type_checker_ptr mk_simple_type_checker(environment const & env, name_predicate const & pred);
+old_type_checker_ptr mk_simple_type_checker(environment const & env, name_predicate const & pred);
 /**
    \brief Generate the format object for <tt>hyps |- conclusion</tt>.
    The given substitution is applied to all elements.