diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index ed821941a..d4abeb230 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -3,11 +3,9 @@ for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
 instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
 object.cpp environment.cpp replace_visitor.cpp io_state.cpp
 normalizer.cpp
-# type_checker.cpp kernel.cpp metavar.cpp
+# type_checker.cpp kernel.cpp
 # justification.cpp unification_constraint.cpp
 # type_checker_justification.cpp pos_info_provider.cpp
-# update_expr.cpp
-# universe_constraints.cpp
 )
 
 target_link_libraries(kernel ${LEAN_LIBS})
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
deleted file mode 100644
index 104cfb58e..000000000
--- a/src/kernel/metavar.cpp
+++ /dev/null
@@ -1,503 +0,0 @@
-/*
-Copyright (c) 2013 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 <limits>
-#include <algorithm>
-#include "util/exception.h"
-#include "kernel/metavar.h"
-#include "kernel/free_vars.h"
-#include "kernel/instantiate.h"
-#include "kernel/occurs.h"
-#include "kernel/for_each_fn.h"
-#include "kernel/find_fn.h"
-
-namespace lean {
-/**
-   \brief Assignment normalization justification. That is, when other assignments are applied to an existing assignment.
-*/
-class normalize_assignment_justification : public justification_cell {
-    context                    m_ctx;
-    expr                       m_expr;
-    std::vector<justification> m_jsts;
-public:
-    normalize_assignment_justification(context const & ctx, expr const & e,
-                                       justification const & jst,
-                                       unsigned num_assignment_jsts, justification const * assignment_jsts):
-        m_ctx(ctx),
-        m_expr(e),
-        m_jsts(assignment_jsts, assignment_jsts + num_assignment_jsts) {
-        m_jsts.push_back(jst);
-        std::reverse(m_jsts.begin(), m_jsts.end());
-    }
-
-    virtual format pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const {
-        unsigned indent = get_pp_indent(opts);
-        format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_expr), false, opts);
-        format r;
-        r += format("Normalize assignment");
-        r += nest(indent, compose(line(), expr_fmt));
-        return r;
-    }
-
-    virtual void get_children(buffer<justification_cell*> & r) const {
-        append(r, m_jsts);
-    }
-
-    virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
-};
-
-void metavar_env_cell::inc_timestamp() {
-    if (m_timestamp == std::numeric_limits<unsigned>::max()) {
-        // This should not happen in real examples. We add it just to be safe.
-        throw exception("metavar_env_cell timestamp overflow");
-    }
-    m_timestamp++;
-}
-
-metavar_env_cell::metavar_env_cell(name const & prefix):
-    m_name_generator(prefix),
-    m_beta_reduce_mv(true),
-    m_timestamp(1),
-    m_rc(0) {
-}
-
-static name g_default_name("M");
-metavar_env_cell::metavar_env_cell():
-    metavar_env_cell(g_default_name) {
-}
-
-metavar_env_cell::metavar_env_cell(metavar_env_cell const & other):
-    m_name_generator(other.m_name_generator),
-    m_metavar_data(other.m_metavar_data),
-    m_beta_reduce_mv(other.m_beta_reduce_mv),
-    m_timestamp(1),
-    m_rc(0) {
-}
-
-expr metavar_env_cell::mk_metavar(context const & ctx, optional<expr> const & type) {
-    inc_timestamp();
-    name m = m_name_generator.next();
-    expr r = ::lean::mk_metavar(m);
-    m_metavar_data.insert(m, data(type, ctx));
-    return r;
-}
-
-context metavar_env_cell::get_context(expr const & m) const {
-    lean_assert(is_metavar(m));
-    lean_assert(!has_local_context(m));
-    return get_context(metavar_name(m));
-}
-
-context metavar_env_cell::get_context(name const & m) const {
-    auto it = m_metavar_data.find(m);
-    lean_assert(it);
-    return it->m_context;
-}
-
-expr metavar_env_cell::get_type(expr const & m) {
-    lean_assert(is_metavar(m));
-    expr t = get_type(metavar_name(m));
-    if (has_local_context(m)) {
-        if (is_metavar(t)) {
-            return update_metavar(t, append(metavar_lctx(m), metavar_lctx(t)));
-        } else {
-            return apply_local_context(t, metavar_lctx(m), metavar_env(this));
-        }
-    } else {
-        return t;
-    }
-}
-
-expr metavar_env_cell::get_type(name const & m) {
-    auto it = m_metavar_data.find(m);
-    lean_assert(it);
-    if (it->m_type) {
-        return *(it->m_type);
-    } else {
-        expr t = mk_metavar(get_context(m));
-        it->m_type = t;
-        return t;
-    }
-}
-
-bool metavar_env_cell::has_type(name const & m) const {
-    auto it = m_metavar_data.find(m);
-    lean_assert(it);
-    return static_cast<bool>(it->m_type);
-}
-
-bool metavar_env_cell::has_type(expr const & m) const {
-    lean_assert(is_metavar(m));
-    return has_type(metavar_name(m));
-}
-
-optional<justification> metavar_env_cell::get_justification(expr const & m) const {
-    lean_assert(is_metavar(m));
-    return get_justification(metavar_name(m));
-}
-
-optional<justification> metavar_env_cell::get_justification(name const & m) const {
-    auto r = get_subst_jst(m);
-    if (r)
-        return optional<justification>(r->second);
-    else
-        return optional<justification>();
-}
-
-bool metavar_env_cell::is_assigned(name const & m) const {
-    auto it = m_metavar_data.find(m);
-    return it && it->m_subst;
-}
-
-bool metavar_env_cell::is_assigned(expr const & m) const {
-    lean_assert(is_metavar(m));
-    return is_assigned(metavar_name(m));
-}
-
-bool metavar_env_cell::assign(name const & m, expr const & t, justification const & jst) {
-    lean_assert(!is_assigned(m));
-    inc_timestamp();
-    justification jst2 = jst;
-    buffer<justification> jsts;
-    expr t2 = instantiate_metavars(t, jsts);
-    if (!jsts.empty()) {
-        jst2 = justification(new normalize_assignment_justification(get_context(m), t, jst,
-                                                                    jsts.size(), jsts.data()));
-    }
-    unsigned ctx_size = get_context_size(m);
-    if (has_metavar(t2)) {
-        bool failed = false;
-        // Make sure the contexts of the metavariables occurring in \c t2 are
-        // not too big.
-        for_each(t2, [&](expr const & e, unsigned offset) {
-                if (is_metavar(e)) {
-                    lean_assert(!is_assigned(e));
-                    unsigned range = free_var_range(e, metavar_env(this));
-                    if (range > ctx_size + offset) {
-                        unsigned extra = range - ctx_size - offset;
-                        auto it2 = m_metavar_data.find(metavar_name(e));
-                        if (it2 == nullptr) {
-                            failed = true;
-                        } else {
-                            unsigned e_ctx_size = it2->m_context.size();
-                            if (e_ctx_size < extra) {
-                                failed = true;
-                            } else {
-                                it2->m_context = it2->m_context.truncate(e_ctx_size - extra);
-                                lean_assert_le(free_var_range(e, metavar_env(this)), ctx_size + offset);
-                            }
-                        }
-                    }
-                }
-                return true;
-            });
-        if (failed)
-            return false;
-    }
-    if (free_var_range(t2, metavar_env(this)) > ctx_size)
-        return false;
-    auto it = m_metavar_data.find(m);
-    lean_assert(it);
-    it->m_subst         = t2;
-    it->m_justification = jst2;
-    return true;
-}
-
-bool metavar_env_cell::assign(name const & m, expr const & t) {
-    justification j;
-    return assign(m, t, j);
-}
-
-bool metavar_env_cell::assign(expr const & m, expr const & t, justification const & j) {
-    lean_assert(is_metavar(m));
-    lean_assert(!has_local_context(m));
-    return assign(metavar_name(m), t, j);
-}
-
-bool metavar_env_cell::assign(expr const & m, expr const & t) {
-    justification j;
-    return assign(m, t, j);
-}
-
-expr apply_local_context(expr const & a, local_context const & lctx, optional<ro_metavar_env> const & menv) {
-    if (lctx) {
-        if (is_metavar(a)) {
-            return mk_metavar(metavar_name(a), append(lctx, metavar_lctx(a)));
-        } else {
-            expr r = apply_local_context(a, tail(lctx), menv);
-            local_entry const & e = head(lctx);
-            if (e.is_lift()) {
-                return lift_free_vars(r, e.s(), e.n(), menv);
-            } else {
-                lean_assert(e.is_inst());
-                return instantiate(r, e.s(), e.v(), menv);
-            }
-        }
-    } else {
-        return a;
-    }
-}
-
-optional<std::pair<expr, justification>> metavar_env_cell::get_subst_jst(expr const & m) const {
-    lean_assert(is_metavar(m));
-    auto p = get_subst_jst(metavar_name(m));
-    if (p) {
-        expr r = p->first;
-        local_context const & lctx = metavar_lctx(m);
-        if (lctx)
-            r = apply_local_context(r, lctx, metavar_env(const_cast<metavar_env_cell*>(this)));
-        return some(mk_pair(r, p->second));
-    } else {
-        return p;
-    }
-}
-
-optional<std::pair<expr, justification>> metavar_env_cell::get_subst_jst(name const & m) const {
-    auto it = const_cast<metavar_env_cell*>(this)->m_metavar_data.find(m);
-    if (it->m_subst) {
-        expr s = *(it->m_subst);
-        if (has_assigned_metavar(s)) {
-            buffer<justification> jsts;
-            expr new_subst = instantiate_metavars(s, jsts);
-            if (!jsts.empty()) {
-                justification new_jst(new normalize_assignment_justification(it->m_context, s, it->m_justification,
-                                                                             jsts.size(), jsts.data()));
-                it->m_justification = new_jst;
-                it->m_subst         = new_subst;
-            }
-        }
-        return optional<std::pair<expr, justification>>(std::pair<expr, justification>(*(it->m_subst), it->m_justification));
-    } else {
-        return optional<std::pair<expr, justification>>();
-    }
-}
-
-optional<expr> metavar_env_cell::get_subst(name const & m) const {
-    auto r = get_subst_jst(m);
-    if (r)
-        return some_expr(r->first);
-    else
-        return none_expr();
-}
-
-optional<expr> metavar_env_cell::get_subst(expr const & m) const {
-    auto r = get_subst_jst(m);
-    if (r)
-        return some_expr(r->first);
-    else
-        return none_expr();
-}
-
-bool metavar_env_cell::has_assigned_metavar(expr const & e) const {
-    if (!has_metavar(e)) {
-        return false;
-    } else {
-        bool result = false;
-        for_each(e, [&](expr const & n, unsigned) {
-                if (result)
-                    return false;
-                if (!has_metavar(n))
-                    return false;
-                if (is_metavar(n)) {
-                    if (is_assigned(n)) {
-                        result = true;
-                        return false;
-                    }
-                    for (auto const & entry : metavar_lctx(n)) {
-                        if (entry.is_inst() && has_assigned_metavar(entry.v())) {
-                            result = true;
-                            return false;
-                        }
-                    }
-                }
-                return true;
-            });
-        return result;
-    }
-}
-
-bool metavar_env_cell::has_metavar(expr const & e, expr const & m) const {
-    if (has_metavar(e)) {
-        lean_assert(is_metavar(m));
-        lean_assert(!is_assigned(m));
-        return static_cast<bool>(find(e, [&](expr const & m2) {
-                    return
-                        is_metavar(m2) &&
-                        ((metavar_name(m) == metavar_name(m2)) ||
-                         (is_assigned(m2) && has_metavar(*get_subst(m2), m)));
-                }));
-    } else {
-        return false;
-    }
-}
-
-class instantiate_metavars_proc : public replace_visitor {
-protected:
-    metavar_env_cell const *  m_menv;
-    buffer<justification> &   m_jsts;
-
-    void push_back(justification const & jst) {
-        if (jst)
-            m_jsts.push_back(jst);
-    }
-
-    virtual expr visit_metavar(expr const & m, context const & ctx) {
-        local_context const & lctx = metavar_lctx(m);
-        if (is_metavar(m) && m_menv->is_assigned(m)) {
-            auto p = m_menv->get_subst_jst(m);
-            lean_assert(p);
-            expr r = p->first;
-            push_back(p->second);
-            if (m_menv->has_assigned_metavar(r)) {
-                return visit(r, ctx);
-            } else {
-                return r;
-            }
-        } else if (std::find_if(lctx.begin(), lctx.end(), [&](local_entry const & e) { return e.is_inst() && m_menv->has_assigned_metavar(e.v()); })
-                   != lctx.end()) {
-            // local context has assigned metavariables
-            buffer<local_entry> new_lctx;
-            for (auto const & e : lctx) {
-                if (e.is_inst())
-                    new_lctx.push_back(mk_inst(e.s(), visit(e.v(), ctx)));
-                else
-                    new_lctx.push_back(e);
-            }
-            return mk_metavar(metavar_name(m), to_list(new_lctx.begin(), new_lctx.end()));
-        } else {
-            return m;
-        }
-    }
-
-    virtual expr visit_app(expr const & e, context const & ctx) {
-        expr const & f = arg(e, 0);
-        if (m_menv->beta_reduce_metavar_application() && is_metavar(f) && m_menv->is_assigned(f)) {
-            buffer<expr> new_args;
-            for (unsigned i = 0; i < num_args(e); i++)
-                new_args.push_back(visit(arg(e, i), ctx));
-            if (is_lambda(new_args[0]))
-                return apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
-            else
-                return mk_app(new_args);
-        } else {
-            return replace_visitor::visit_app(e, ctx);
-        }
-    }
-
-public:
-    instantiate_metavars_proc(metavar_env_cell const * menv, buffer<justification> & jsts):
-        m_menv(menv),
-        m_jsts(jsts) {
-    }
-};
-
-expr metavar_env_cell::instantiate_metavars(expr const & e, buffer<justification> & jsts) const {
-    if (!has_metavar(e)) {
-        return e;
-    } else {
-        expr r = instantiate_metavars_proc(this, jsts)(e);
-        lean_assert(!has_assigned_metavar(r));
-        return r;
-    }
-}
-
-context metavar_env_cell::instantiate_metavars(context const & ctx) const {
-    buffer<context_entry> new_entries;
-    auto it  = ctx.begin();
-    auto end = ctx.end();
-    for (; it != end; ++it) {
-        auto n = it->get_name();
-        auto d = it->get_domain();
-        auto b = it->get_body();
-        if (d && b)
-            new_entries.emplace_back(n, instantiate_metavars(*d), instantiate_metavars(*b));
-        else if (d)
-            new_entries.emplace_back(n, instantiate_metavars(*d));
-        else
-            new_entries.emplace_back(n, none_expr(), instantiate_metavars(*b));
-    }
-    return context(new_entries.size(), new_entries.data());
-}
-
-template<typename MEnv>
-bool cached_metavar_env_tpl<MEnv>::update(optional<MEnv> const & menv) {
-    if (!menv) {
-        m_menv = optional<MEnv>();
-        if (m_timestamp != 0) {
-            m_timestamp = 0;
-            return true;
-        } else {
-            return false;
-        }
-    } else {
-        unsigned new_timestamp = (*menv)->get_timestamp();
-        if (m_menv != menv || m_timestamp != new_timestamp) {
-            m_menv      = menv;
-            m_timestamp = new_timestamp;
-            return true;
-        } else {
-            return false;
-        }
-    }
-}
-template class cached_metavar_env_tpl<metavar_env>;
-template class cached_metavar_env_tpl<ro_metavar_env>;
-
-local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
-    if (n == 0)
-        return lctx;
-    if (lctx) {
-        local_entry e = head(lctx);
-        // Simplification rule
-        //    lift:s2:n2 lift:s1:n1 --->  lift:s1:n1+n2   when s1 <= s2 <= s1 + n1
-        if (e.is_lift() && e.s() <= s && s <= e.s() + e.n()) {
-            return add_lift(tail(lctx), e.s(), e.n() + n);
-        }
-    }
-    return cons(mk_lift(s, n), lctx);
-}
-
-expr add_lift(expr const & m, unsigned s, unsigned n, optional<ro_metavar_env> const & menv) {
-    if (menv && s >= free_var_range(m, *menv))
-        return m;
-    return update_metavar(m, add_lift(metavar_lctx(m), s, n));
-}
-
-local_context add_inst(local_context const & lctx, unsigned s, expr const & v) {
-    if (lctx) {
-        local_entry e = head(lctx);
-        if (e.is_lift() && e.s() <= s && s < e.s() + e.n()) {
-            return add_lift(tail(lctx), e.s(), e.n() - 1);
-        }
-        // Simplifications such as
-        //   inst:4 #6  lift:5:3  -->  lift:4:2
-        //   inst:3 #7  lift:4:5 -->   lift:3:4
-        // General rule is:
-        //   inst:(s-1) #(s+n-2)  lift:s:n  --> lift:s-1:n-1
-        if (e.is_lift() && is_var(v) && e.s() > 0 && s == e.s() - 1 && e.s() + e.n() > 2 && var_idx(v) == e.s() + e.n() - 2) {
-            return add_lift(tail(lctx), e.s() - 1, e.n() - 1);
-        }
-    }
-    return cons(mk_inst(s, v), lctx);
-}
-
-expr add_inst(expr const & m, unsigned s, expr const & v, optional<ro_metavar_env> const & menv) {
-    if (menv && s >= free_var_range(m, *menv))
-        return m;
-    return update_metavar(m, add_inst(metavar_lctx(m), s, v));
-}
-
-bool has_local_context(expr const & m) {
-    return static_cast<bool>(metavar_lctx(m));
-}
-
-expr pop_meta_context(expr const & m) {
-    lean_assert(has_local_context(m));
-    return update_metavar(m, tail(metavar_lctx(m)));
-}
-}
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
deleted file mode 100644
index 26a7635e4..000000000
--- a/src/kernel/metavar.h
+++ /dev/null
@@ -1,389 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <utility>
-#include "util/rc.h"
-#include "util/pair.h"
-#include "util/splay_map.h"
-#include "util/name_generator.h"
-#include "kernel/expr.h"
-#include "kernel/context.h"
-#include "kernel/justification.h"
-#include "kernel/replace_visitor.h"
-
-namespace lean {
-/**
-   \brief Metavar environment (cell). It is an auxiliary datastructure used for:
-
-   1- Creating metavariables.
-   2- Storing their types and the contexts where they were created.
-   3- Storing substitutions.
-*/
-class metavar_env_cell {
-    friend class metavar_env;
-    struct data {
-        optional<expr> m_subst;         // substitution
-        optional<expr> m_type;          // type of the metavariable
-        context        m_context;       // context where the metavariable was defined
-        justification  m_justification; // justification for assigned metavariables.
-        data(optional<expr> const & t = none_expr(), context const & ctx = context()):m_type(t), m_context(ctx) {}
-    };
-    typedef splay_map<name, data, name_quick_cmp> name2data;
-
-    name_generator     m_name_generator;
-    name2data          m_metavar_data;
-    // If the following flag is true, then beta-reduction is automatically applied
-    // when we apply a substitution containing ?m <- fun (x : T), ...
-    // to an expression containing (?m a)
-    // The motivation is that higher order unification and matching produces a
-    // bunch of assignments of the form ?m <- fun (x : T), ...
-    bool               m_beta_reduce_mv;
-    unsigned           m_timestamp;
-    MK_LEAN_RC();
-
-    static bool has_metavar(expr const & e) { return ::lean::has_metavar(e); }
-    void dealloc() { delete this; }
-    void inc_timestamp();
-public:
-    metavar_env_cell();
-    metavar_env_cell(name const & prefix);
-    metavar_env_cell(metavar_env_cell const & other);
-
-    bool beta_reduce_metavar_application() const { return m_beta_reduce_mv; }
-    void set_beta_reduce_metavar_application(bool f) { m_beta_reduce_mv = f; }
-
-    /**
-       \brief The timestamp is increased whenever this environment is
-       updated.
-
-       \remark The result is always greater than 0.
-    */
-    unsigned get_timestamp() const { return m_timestamp; }
-
-    /**
-       \brief Create a new metavariable in the given context and with the given type.
-    */
-    expr mk_metavar(context const & ctx = context(), optional<expr> const & type = none_expr());
-
-    /**
-       \brief Return the context where the given metavariable was created.
-       \pre is_metavar(m)
-       \pre !has_local_context(m)
-    */
-    context get_context(expr const & m) const;
-    context get_context(name const & m) const;
-
-    unsigned get_context_size(expr const & m) const { return get_context(m).size(); }
-    unsigned get_context_size(name const & m) const { return get_context(m).size(); }
-
-    /**
-       \brief Return the type of the given metavariable.
-       \pre is_metavar(m)
-
-       \remark If \c m does not have a type associated with it, then a new
-       metavariable is created to represent the type of \c m.
-
-       \remark If \c m has a local context, then the local context is applied.
-    */
-    expr get_type(expr const & m);
-    expr get_type(name const & m);
-
-    /**
-        \brief Return true iff \c m has a type associated with it.
-        \pre is_metavar(m)
-    */
-    bool has_type(expr const & m) const;
-    bool has_type(name const & m) const;
-
-    /**
-       \brief Return the substitution and justification for the given metavariable.
-    */
-    optional<std::pair<expr, justification>> get_subst_jst(name const & m) const;
-    optional<std::pair<expr, justification>> get_subst_jst(expr const & m) const;
-
-    /**
-       \brief Return the justification for an assigned metavariable.
-       \pre is_metavar(m)
-    */
-    optional<justification> get_justification(expr const & m) const;
-    optional<justification> get_justification(name const & m) const;
-
-    /**
-       \brief Return true iff the metavariable named \c m is assigned in this substitution.
-    */
-    bool is_assigned(name const & m) const;
-
-    /**
-       \brief Return true if the given metavariable is assigned in this
-       substitution.
-
-       \pre is_metavar(m)
-    */
-    bool is_assigned(expr const & m) const;
-
-    /**
-       \brief Assign metavariable named \c m.
-
-       \pre !is_assigned(m)
-
-       \remark The method returns false if the assignment cannot be performed
-       because \c t contain free variables that are not available in the context
-       associated with \c m.
-    */
-    bool assign(name const & m, expr const & t, justification const & j);
-    bool assign(name const & m, expr const & t);
-
-    /**
-       \brief Assign metavariable \c m to \c t.
-
-       \remark The method returns false if the assignment cannot be performed
-       because \c t contain free variables that are not available in the context
-       associated with \c m.
-
-       \pre is_metavar(m)
-       \pre !has_meta_context(m)
-       \pre !is_assigned(m)
-    */
-    bool assign(expr const & m, expr const & t, justification const & j);
-    bool assign(expr const & m, expr const & t);
-
-    /**
-       \brief Return the substitution associated with the given metavariable
-       in this substitution.
-
-       \pre is_metavar(m)
-    */
-    optional<expr> get_subst(expr const & m) const;
-    optional<expr> get_subst(name const & m) const;
-
-    /**
-       \brief Apply f to each substitution in the metavariable environment.
-    */
-    template<typename F>
-    void for_each_subst(F f) const {
-        m_metavar_data.for_each([&](name const & k, data const & d) {
-                if (d.m_subst)
-                    f(k, *(d.m_subst));
-            });
-    }
-
-    /**
-       \brief Return true iff \c e has a metavariable that is assigned in \c menv.
-    */
-    bool has_assigned_metavar(expr const & e) const;
-
-    /**
-       \brief Return true iff \c e contains the metavariable \c m.
-       The substitutions in this metavar environment are taken into account.
-
-       \brief is_metavar(m)
-    */
-    bool has_metavar(expr const & e, expr const & m) const;
-
-   /**
-      \brief Instantiate the metavariables occurring in \c e with the substitutions
-      provided by \c menv. Store the justification of replace variables in jsts.
-   */
-    expr instantiate_metavars(expr const & e, buffer<justification> & jsts) const;
-    inline expr instantiate_metavars(expr const & e) const {
-        buffer<justification> tmp;
-        return instantiate_metavars(e, tmp);
-    }
-    context instantiate_metavars(context const & ctx) const;
-};
-
-class ro_metavar_env;
-/**
-   \brief Reference to metavariable environment (cell).
-*/
-class metavar_env {
-    friend class optional<metavar_env>;
-    friend class ro_metavar_env;
-    friend class metavar_env_cell;
-    metavar_env_cell * m_ptr;
-    explicit metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
-public:
-    metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
-    metavar_env(name const & prefix):m_ptr(new metavar_env_cell(prefix)) { m_ptr->inc_ref(); }
-    metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    metavar_env(metavar_env && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
-    ~metavar_env() { if (m_ptr) m_ptr->dec_ref(); }
-    metavar_env & operator=(metavar_env const & s) { LEAN_COPY_REF(s); }
-    metavar_env & operator=(metavar_env && s) { LEAN_MOVE_REF(s); }
-    metavar_env_cell * operator->() const { return m_ptr; }
-    metavar_env_cell & operator*() const { return *m_ptr; }
-    metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
-    friend bool is_eqp(metavar_env const & menv1, metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
-    friend bool operator==(metavar_env const & menv1, metavar_env const & menv2) { return is_eqp(menv1, menv2); }
-    typedef metavar_env_cell * ptr;
-};
-
-SPECIALIZE_OPTIONAL_FOR_SMART_PTR(metavar_env)
-inline optional<metavar_env> none_menv() { return optional<metavar_env>(); }
-inline optional<metavar_env> some_menv(metavar_env const & e) { return optional<metavar_env>(e); }
-inline optional<metavar_env> some_menv(metavar_env && e) { return optional<metavar_env>(std::forward<metavar_env>(e)); }
-
-inline expr instantiate_metavars(optional<metavar_env> const & menv, expr const & e) {
-    if (menv)
-        return (*menv)->instantiate_metavars(e);
-    else
-        return e;
-}
-
-inline context instantiate_metavars(optional<metavar_env> const & menv, context const & ctx) {
-    if (menv)
-        return (*menv)->instantiate_metavars(ctx);
-    else
-        return ctx;
-}
-
-/**
-   \brief Read-only reference to metavariable environment (cell).
-*/
-class ro_metavar_env {
-    friend class optional<ro_metavar_env>;
-    friend class metavar_env;
-    metavar_env_cell * m_ptr;
-    explicit ro_metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    friend class type_checker;
-    /*
-      \brief (Hack) The following two methods are used by the type_checker. Some methods
-      in the type checker only need read-only access when unification constraints are not
-      used. For these methods, we can relax the interface and accept a read-only metavariable
-      environment. However, the type checker internally uses the read-write version. So,
-      this constructor is a hack to workaround that.
-    */
-    static optional<metavar_env> const & to_rw(optional<ro_metavar_env> const & menv) { return reinterpret_cast<optional<metavar_env> const &>(menv); }
-    metavar_env const & to_rw() const { return reinterpret_cast<metavar_env const&>(*this); }
-public:
-    ro_metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
-    ro_metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    ro_metavar_env(ro_metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    ro_metavar_env(ro_metavar_env && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
-    ~ro_metavar_env() { if (m_ptr) m_ptr->dec_ref(); }
-    ro_metavar_env & operator=(ro_metavar_env const & s) { LEAN_COPY_REF(s); }
-    ro_metavar_env & operator=(ro_metavar_env && s) { LEAN_MOVE_REF(s); }
-    metavar_env_cell const * operator->() const { return m_ptr; }
-    metavar_env_cell const & operator*() const { return *m_ptr; }
-    metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
-    friend bool is_eqp(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
-    friend bool operator==(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return is_eqp(menv1, menv2); }
-    typedef metavar_env_cell const * ptr;
-};
-
-SPECIALIZE_OPTIONAL_FOR_SMART_PTR(ro_metavar_env)
-inline optional<ro_metavar_env> none_ro_menv() { return optional<ro_metavar_env>(); }
-inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env const & e) { return optional<ro_metavar_env>(e); }
-inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env && e) { return optional<ro_metavar_env>(std::forward<ro_metavar_env>(e)); }
-inline optional<ro_metavar_env> const & to_ro_menv(optional<metavar_env> const & menv) { return reinterpret_cast<optional<ro_metavar_env> const &>(menv); }
-
-/**
-   \brief Template for creating a cached reference to a metavariable
-   environment + timestamp at the time of the caching. This object may
-   also cache optional references.
-
-   We use this template for cached_metavar_env and cached_ro_metavar_env
-*/
-template<typename MEnv>
-class cached_metavar_env_tpl {
-    optional<MEnv> m_menv;
-    unsigned       m_timestamp;
-public:
-    cached_metavar_env_tpl():m_timestamp(0) {}
-    void clear() { m_menv = optional<MEnv>(); m_timestamp = 0; }
-    /**
-       \brief Updated the cached value with menv.
-       Return true if menv is different from the the cached metavar_env, or if
-       the timestamp is different.
-    */
-    bool update(optional<MEnv> const & menv);
-    bool update(MEnv const & menv) { return update(optional<MEnv>(menv)); }
-    explicit operator bool() const { return static_cast<bool>(m_menv); }
-    optional<MEnv> const & to_some_menv() const { return m_menv; }
-    MEnv operator*() const { return *m_menv; }
-    typename MEnv::ptr operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); }
-};
-
-class cached_metavar_env : public cached_metavar_env_tpl<metavar_env> {
-public:
-    optional<ro_metavar_env> const & to_some_ro_menv() const { return to_ro_menv(to_some_menv()); }
-};
-
-typedef cached_metavar_env_tpl<ro_metavar_env> cached_ro_metavar_env;
-
-/**
-   \brief Apply the changes in \c lctx to \c a.
-*/
-expr apply_local_context(expr const & a, local_context const & lctx, optional<ro_metavar_env> const & menv);
-inline expr apply_local_context(expr const & a, local_context const & lctx, ro_metavar_env const & menv) { return apply_local_context(a, lctx, some_ro_menv(menv)); }
-inline expr apply_local_context(expr const & a, local_context const & lctx) { return apply_local_context(a, lctx, none_ro_menv()); }
-
-/**
-    \brief Extend the local context \c lctx with the entry <tt>lift:s:n</tt>
-*/
-local_context add_lift(local_context const & lctx, unsigned s, unsigned n);
-
-/**
-   \brief Add a lift:s:n operation to the context of the given metavariable.
-
-   \pre is_metavar(m)
-
-   \remark If menv is not none, then we use \c free_var_range to compute the free variables that may
-   occur in \c m. If s > the maximum free variable that occurs in \c m, then
-   we do not add a lift local entry to the local context.
-*/
-expr add_lift(expr const & m, unsigned s, unsigned n, optional<ro_metavar_env> const & menv);
-inline expr add_lift(expr const & m, unsigned s, unsigned n) { return add_lift(m, s, n, none_ro_menv()); }
-inline expr add_lift(expr const & m, unsigned s, unsigned n, ro_metavar_env const & menv) { return add_lift(m, s, n, some_ro_menv(menv)); }
-
-/**
-   \brief Extend the local context \c lctx with the entry <tt>inst:s v</tt>
-*/
-local_context add_inst(local_context const & lctx, unsigned s, expr const & v);
-
-/**
-   \brief Add an inst:s:v operation to the context of the given metavariable.
-
-   \pre is_metavar(m)
-
-   \remark If menv is not none, then we use \c free_var_range to compute the free variables that may
-   occur in \c m. If s > the maximum free variable that occurs in \c m, then
-   we do not add an inst local entry to the local context.
-*/
-expr add_inst(expr const & m, unsigned s, expr const & v, optional<ro_metavar_env> const & menv);
-inline expr add_inst(expr const & m, unsigned s, expr const & v) { return add_inst(m, s, v, none_ro_menv()); }
-inline expr add_inst(expr const & m, unsigned s, expr const & v, ro_metavar_env const & menv) { return add_inst(m, s, v, some_ro_menv(menv)); }
-
-/**
-   \brief Return true iff the given metavariable has a non-empty
-   local context associated with it.
-
-   \pre is_metavar(m)
-*/
-bool has_local_context(expr const & m);
-
-/**
-   \brief Return the same metavariable, but the head of the context is removed.
-
-   \pre is_metavar(m)
-   \pre has_meta_context(m)
-*/
-expr pop_meta_context(expr const & m);
-
-/**
-   \brief Return true iff \c e has a metavariable that is assigned in \c menv.
-*/
-bool has_assigned_metavar(expr const & e, ro_metavar_env const & menv);
-
-/**
-   \brief Return true iff \c e contains the metavariable \c m.
-   The substitutions in \c menv are taken into account.
-
-   \brief is_metavar(m)
-*/
-bool has_metavar(expr const & e, expr const & m, ro_metavar_env const & menv);
-}
diff --git a/src/kernel/universe_constraints.cpp b/src/kernel/universe_constraints.cpp
deleted file mode 100644
index ed3317d36..000000000
--- a/src/kernel/universe_constraints.cpp
+++ /dev/null
@@ -1,97 +0,0 @@
-/*
-Copyright (c) 2013 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/safe_arith.h"
-#include "util/pair.h"
-#include "util/buffer.h"
-#include "kernel/universe_constraints.h"
-
-namespace lean {
-optional<int> universe_constraints::get_distance(name const & n1, name const & n2) const {
-    auto it = m_distances.find(mk_pair(n1, n2));
-    if (it != m_distances.end())
-        return optional<int>(it->second);
-    else
-        return optional<int>();
-}
-
-void universe_constraints::add_var(name const & n) {
-    lean_assert(!get_distance(n, n));
-    m_distances[mk_pair(n, n)] = 0;
-    m_outgoing_edges[n].emplace_back(n, 0);
-    m_incoming_edges[n].emplace_back(n, 0);
-}
-
-bool universe_constraints::contains(name const & n) const {
-    return static_cast<bool>(get_distance(n, n));
-}
-
-bool universe_constraints::is_implied(name const & n1, name const & n2, int k) const {
-    auto d = get_distance(n1, n2);
-    return d && *d >= k;
-}
-
-bool universe_constraints::is_consistent(name const & n1, name const & n2, int k) const {
-    // we just check if n2 >= n1 - k + 1 is not implied
-    return !is_implied(n2, n1, safe_add(safe_sub(0, k), 1));
-}
-
-bool universe_constraints::overflows(name const & n1, name const & n2, int k) const {
-    try {
-        auto it1 = m_incoming_edges.find(n1);
-        if (it1 != m_incoming_edges.end()) {
-            for (auto const & in : it1->second)
-                safe_add(in.second, k);
-        }
-        auto it2 = m_outgoing_edges.find(n2);
-        if (it2 != m_outgoing_edges.end()) {
-            for (auto const & out : it2->second)
-                safe_add(out.second, k);
-        }
-        return false;
-    } catch (...) {
-        return true;
-    }
-}
-
-/**
-    \brief Add the pair (n, k) to entries if it does not contain an entry (n, k').
-    Otherwise, replace entry (n, k') with (n, k).
-*/
-static void updt_entry(std::vector<std::pair<name, int>> & entries, name const & n, int k) {
-    auto it = std::find_if(entries.begin(), entries.end(), [&](std::pair<name, int> const & p) { return p.first == n; });
-    if (it == entries.end())
-        entries.emplace_back(n, k);
-    else
-        it->second = k;
-}
-
-void universe_constraints::add_constraint(name const & n1, name const & n2, int k) {
-    lean_assert(contains(n1));
-    lean_assert(contains(n2));
-    lean_assert(is_consistent(n1, n2, k));
-    if (is_implied(n1, n2, k))
-        return; // redundant
-    buffer<std::tuple<name, name, int>> to_add;
-    for (auto const & in : m_incoming_edges[n1])
-        to_add.emplace_back(in.first, n2, safe_add(in.second, k));
-    for (auto const & out : m_outgoing_edges[n2])
-        to_add.emplace_back(n1, out.first, safe_add(out.second, k));
-    for (auto const & e : to_add) {
-        name const & from = std::get<0>(e);
-        name const & to   = std::get<1>(e);
-        int new_k         = std::get<2>(e);
-        auto old_k        = get_distance(from, to);
-        if (!old_k || new_k > *old_k) {
-            updt_entry(m_outgoing_edges[from], to, new_k);
-            updt_entry(m_incoming_edges[to], from, new_k);
-            m_distances[mk_pair(from, to)] = new_k;
-        }
-    }
-}
-}
diff --git a/src/kernel/universe_constraints.h b/src/kernel/universe_constraints.h
deleted file mode 100644
index afca4717b..000000000
--- a/src/kernel/universe_constraints.h
+++ /dev/null
@@ -1,73 +0,0 @@
-/*
-Copyright (c) 2013 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_map>
-#include <utility>
-#include <functional>
-#include <vector>
-#include "util/name.h"
-#include "util/hash.h"
-#include "util/name_map.h"
-#include "util/optional.h"
-
-namespace lean {
-/**
-   \brief Store the set of universe constraints.
-
-   It is based on Floyd-Warshall all-pairs shortest path algorithm.
-*/
-class universe_constraints {
-    typedef std::pair<name, int> edge;
-    typedef std::vector<edge> edges;
-    typedef name_map<edges> node_to_edges;
-    typedef std::pair<name, name> name_pair;
-    struct name_pair_hash_fn {
-        unsigned operator()(name_pair const & p) const { return hash(p.first.hash(), p.second.hash()); }
-    };
-    typedef std::unordered_map<name_pair, int, name_pair_hash_fn, std::equal_to<name_pair>> distances;
-    node_to_edges m_incoming_edges;
-    node_to_edges m_outgoing_edges;
-    distances     m_distances;
-public:
-    /**
-       \brief Add a new variable.
-
-       \pre The variables does not exist in this set of constraints.
-    */
-    void add_var(name const & n);
-    /**
-       \brief Return true iff this set of constraints contains the variable n.
-       That is, it was added using add_var.
-    */
-    bool contains(name const & n) const;
-    /** \brief Return true iff n1 >= n2 + k is implied by this set of constraints. */
-    bool is_implied(name const & n1, name const & n2, int k) const;
-    /** \brief Return true iff n1 < n2 + k is not implied by this set of constraints. */
-    bool is_consistent(name const & n1, name const & n2, int k) const;
-    /**
-       \brief Return true iff the constraint n1 >= n2 + k produces an integer overflow when added
-       to the set of constraints.
-    */
-    bool overflows(name const & n1, name const & n2, int k) const;
-    /**
-        \brief Add new constraint n1 >= n2 + k.
-
-        \pre is_consistent(n1, n2, k)
-        \pre contains(n1)
-        \pre contains(n2)
-    */
-    void add_constraint(name const & n1, name const & n2, int k);
-    /**
-       \brief Return the "distance" between n1 and n2.
-       That is, the best k s.t. n1 >= n2 + k is implied by this set of constraints
-       but n1 >= n2 + k + i is not for any i > 0.
-
-       If there is no such k, then return none.
-    */
-    optional<int> get_distance(name const & n1, name const & n2) const;
-};
-}
diff --git a/src/kernel/value.h b/src/kernel/value.h
deleted file mode 100644
index bb0e43b48..000000000
--- a/src/kernel/value.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-/**
-   \brief Base class for values that have a hierarchical attached to it.
-*/
-class named_value : public value {
-    name m_name;
-public:
-    named_value(name const & n):m_name(n) {}
-    virtual ~named_value() {}
-    virtual name get_name() const { return m_name; }
-    virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return true; } // NOLINT
-};
-
-/**
-   \brief Base class for values that have a hierarchical name and a type
-   attached to it.
-*/
-class const_value : public named_value {
-    expr m_type;
-public:
-    const_value(name const & n, expr const & t):named_value(n), m_type(t) {}
-    virtual ~const_value() {}
-    virtual expr get_type() const { return m_type; }
-};
-}