diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt
index 209a739d68..d0f3d1fba1 100644
--- a/src/library/blast/CMakeLists.txt
+++ b/src/library/blast/CMakeLists.txt
@@ -1,2 +1,2 @@
-add_library(blast OBJECT expr.cpp branch.cpp state.cpp infer_type.cpp blast.cpp
+add_library(blast OBJECT expr.cpp branch.cpp state.cpp blast.cpp
   blast_tactic.cpp init_module.cpp)
diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 81652b452a..94e80920c3 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -4,18 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <vector>
+#include "util/sstream.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/type_checker.h"
 #include "library/replace_visitor.h"
 #include "library/util.h"
 #include "library/reducible.h"
 #include "library/normalize.h"
+#include "library/class.h"
+#include "library/type_inference.h"
 #include "library/projection.h"
+#include "library/tactic/goal.h"
 #include "library/blast/expr.h"
 #include "library/blast/state.h"
-#include "library/blast/infer_type.h"
 #include "library/blast/blast.h"
-#include "library/blast/blast_context.h"
 #include "library/blast/blast_exception.h"
 
 namespace lean {
@@ -23,16 +26,148 @@ namespace blast {
 static name * g_prefix = nullptr;
 
 class blastenv {
+    friend class scope;
     environment                m_env;
     io_state                   m_ios;
+    name_generator             m_ngen;
     name_set                   m_lemma_hints;
     name_set                   m_unfold_hints;
     name_map<level>            m_uvar2uref;    // map global universe metavariables to blast uref's
     name_map<pair<expr, expr>> m_mvar2meta_mref; // map global metavariables to blast mref's
     name_predicate             m_not_reducible_pred;
+    name_predicate             m_class_pred;
+    name_predicate             m_instance_pred;
     name_map<projection_info>  m_projection_info;
     state                      m_curr_state;   // current state
 
+    class ti : public type_inference {
+        blastenv &         m_benv;
+        std::vector<state> m_stack;
+    public:
+        ti(blastenv & benv):
+            type_inference(benv.m_env, benv.m_ios),
+            m_benv(benv) {}
+
+        virtual bool is_extra_opaque(name const & n) const {
+            // TODO(Leo): class and instances
+            return m_benv.m_not_reducible_pred(n) || m_benv.m_projection_info.contains(n);
+        }
+
+        virtual expr mk_tmp_local(expr const & type, binder_info const & bi) {
+            name n = m_benv.m_ngen.next();
+            return blast::mk_local(n, n, type, bi);
+        }
+
+        virtual bool is_tmp_local(expr const & e) const {
+            return blast::is_local(e);
+        }
+
+        virtual bool is_uvar(level const & l) const {
+            return blast::is_uref(l);
+        }
+
+        virtual bool is_mvar(expr const & e) const {
+            return blast::is_mref(e);
+        }
+
+        virtual level const * get_assignment(level const & u) const {
+            return m_benv.m_curr_state.get_uref_assignment(u);
+        }
+
+        virtual expr const * get_assignment(expr const & m) const {
+            return m_benv.m_curr_state.get_mref_assignment(m);
+        }
+
+        virtual void update_assignment(level const & u, level const & v) {
+            m_benv.m_curr_state.assign_uref(u, v);
+        }
+
+        virtual void update_assignment(expr const & m, expr const & v) {
+            m_benv.m_curr_state.assign_mref(m, v);
+        }
+
+        virtual bool validate_assignment(expr const & m, buffer<expr> const & locals, expr const & v) {
+            // We must check
+            //   1. All href in new_v are in the context of m.
+            //   2. The context of any (unassigned) mref in new_v must be a subset of the context of m.
+            //      If it is not we force it to be.
+            //   3. Any local constant occurring in new_v occurs in locals
+            //   4. m does not occur in new_v
+            state & s = m_benv.m_curr_state;
+            metavar_decl const * d = s.get_metavar_decl(m);
+            lean_assert(d);
+            bool ok = true;
+            for_each(v, [&](expr const & e, unsigned) {
+                    if (!ok)
+                        return false; // stop search
+                    if (is_href(e)) {
+                        if (!d->contains_href(e)) {
+                            ok = false; // failed 1
+                            return false;
+                        }
+                    } else if (blast::is_local(e)) {
+                        if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) {
+                                    return local_index(a) != local_index(e); })) {
+                            ok = false; // failed 3
+                            return false;
+                        }
+                    } else if (is_mref(e)) {
+                        if (m == e) {
+                            ok = false; // failed 4
+                            return false;
+                        }
+                        s.restrict_mref_context_using(e, m); // enforce 2
+                        return false;
+                    }
+                    return true;
+                });
+            return ok;
+        }
+
+        /** \brief Return the type of a local constant (local or not).
+            \remark This method allows the customer to store the type of local constants
+            in a different place. */
+        virtual expr infer_local(expr const & e) const {
+            if (is_href(e)) {
+                branch const & b = m_benv.m_curr_state.get_main_branch();
+                hypothesis const * h = b.get(e);
+                lean_assert(h);
+                return h->get_type();
+            } else {
+                return mlocal_type(e);
+            }
+        }
+
+        virtual expr infer_metavar(expr const & m) const {
+            state const & s = m_benv.m_curr_state;
+            metavar_decl const * d = s.get_metavar_decl(m);
+            lean_assert(d);
+            return d->get_type();
+        }
+
+        virtual level mk_uvar() {
+            return m_benv.m_curr_state.mk_uref();
+        }
+
+        virtual expr mk_mvar(expr const & type) {
+            return m_benv.m_curr_state.mk_metavar(type);
+        }
+
+        virtual void push() {
+            // TODO(Leo): we only need to save the assignment and metavar_decls.
+            m_stack.push_back(m_benv.m_curr_state);
+        }
+
+        virtual void pop() {
+            m_benv.m_curr_state = m_stack.back();
+            m_stack.pop_back();
+        }
+
+        virtual void commit() {
+            m_stack.pop_back();
+        }
+    };
+
     class to_blast_expr_fn : public replace_visitor {
         type_checker                 m_tc;
         state &                      m_state;
@@ -219,15 +354,22 @@ class blastenv {
         return s;
     }
 
+    ti m_ti;
+
 public:
     blastenv(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds):
-        m_env(env), m_ios(ios), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)),
-        m_not_reducible_pred(mk_not_reducible_pred(env)) {
+        m_env(env), m_ios(ios), m_ngen(*g_prefix), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)),
+        m_not_reducible_pred(mk_not_reducible_pred(env)),
+        m_class_pred(mk_class_pred(env)),
+        m_instance_pred(mk_instance_pred(env)),
+        m_ti(*this) {
     }
 
     optional<expr> operator()(goal const & g) {
         m_curr_state = to_state(g);
 
+        // TODO(Leo): set local context for type class resolution at ti
+
         // TODO(Leo): blast main loop
         display("Blast tactic initial state\n");
         display_curr_state();
@@ -250,6 +392,17 @@ public:
     projection_info const * get_projection_info(name const & n) const {
         return m_projection_info.find(n);
     }
+
+    name mk_fresh_local_name() { return m_ngen.next(); }
+    expr mk_fresh_local(expr const & type, binder_info const & bi) {
+        name n = m_ngen.next();
+        return blast::mk_local(n, n, type, bi);
+    }
+    expr whnf(expr const & e) { return m_ti.whnf(e); }
+    expr infer_type(expr const & e) { return m_ti.infer(e); }
+    bool is_prop(expr const & e) { return m_ti.is_prop(e); }
+    bool is_def_eq(expr const & e1, expr const & e2) { return m_ti.is_def_eq(e1, e2); }
+    optional<expr> mk_class_instance(expr const & e) { return m_ti.mk_class_instance(e); }
 };
 
 LEAN_THREAD_PTR(blastenv, g_blastenv);
@@ -285,6 +438,41 @@ projection_info const * get_projection_info(name const & n) {
     return g_blastenv->get_projection_info(n);
 }
 
+expr whnf(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->whnf(e);
+}
+
+expr infer_type(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->infer_type(e);
+}
+
+bool is_prop(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->is_prop(e);
+}
+
+bool is_def_eq(expr const & e1, expr const & e2) {
+    lean_assert(g_blastenv);
+    return g_blastenv->is_def_eq(e1, e2);
+}
+
+optional<expr> mk_class_instance(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_class_instance(e);
+}
+
+name mk_fresh_local_name() {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_fresh_local_name();
+}
+
+expr mk_fresh_local(expr const & type, binder_info const & bi) {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_fresh_local(type, bi);
+}
+
 void display_curr_state() {
     curr_state().display(env(), ios());
     display("\n");
@@ -298,58 +486,27 @@ void display(sstream const & msg) {
     ios().get_diagnostic_channel() << msg.str();
 }
 
-/** \brief Auxiliary object to interface blast state with existing kernel extensions */
-class ext_context : public extension_context {
-    name_generator m_ngen;
-public:
-    virtual environment const & env() const { return env(); }
-
-    virtual pair<expr, constraint_seq> whnf(expr const & e) {
-        return mk_pair(blast::whnf(e), constraint_seq());
-    }
-
-    virtual pair<bool, constraint_seq> is_def_eq(expr const & e1, expr const & e2, delayed_justification &) {
-        return mk_pair(blast::is_def_eq(e1, e2), constraint_seq());
-    }
-
-    virtual pair<expr, constraint_seq> check_type(expr const & e, bool) {
-        return mk_pair(blast::infer_type(e), constraint_seq());
-    }
-
-    virtual name mk_fresh_name() {
-        return m_ngen.next();
-    }
-
-    virtual optional<expr> is_stuck(expr const &) {
-        return none_expr();
-    }
-};
-
-LEAN_THREAD_PTR(ext_context, g_ext_context);
-struct scope_ext_context {
-    ext_context * m_prev_context;
-public:
-    scope_ext_context(ext_context & c):m_prev_context(g_ext_context) { g_ext_context = &c; }
-    ~scope_ext_context() { g_ext_context = m_prev_context; }
-};
-
-extension_context & ext_ctx() {
-    lean_assert(g_ext_context);
-    return *g_ext_context;
+scope::scope():m_keep(false) {
+    lean_assert(g_blastenv);
+    g_blastenv->m_ti.push();
 }
 
-name mk_fresh_local_name() {
-    lean_assert(g_ext_context);
-    return g_ext_context->mk_fresh_name();
+scope::~scope() {
+    if (m_keep)
+        g_blastenv->m_ti.commit();
+    else
+        g_blastenv->m_ti.pop();
+}
+
+void scope::commit() {
+    m_keep = true;
 }
 }
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g) {
     blast::scope_hash_consing scope1;
     blast::blastenv b(env, ios, ls, ds);
-    blast::ext_context x;
     blast::scope_blastenv    scope2(b);
-    blast::scope_ext_context scope3(x);
     return b(g);
 }
 void initialize_blast() {
diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h
index 372d5288c3..9e3a889c43 100644
--- a/src/library/blast/blast.h
+++ b/src/library/blast/blast.h
@@ -5,9 +5,63 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/tactic/goal.h"
+#include "kernel/environment.h"
+#include "library/io_state.h"
+#include "library/blast/state.h"
 
 namespace lean {
+struct projection_info;
+class goal;
+namespace blast {
+/** \brief Return the thread local environment being used by the blast tactic. */
+environment const & env();
+/** \brief Return the thread local io_state being used by the blast tactic. */
+io_state const & ios();
+/** \brief Return the thread local current state begin processed by the blast tactic. */
+state & curr_state();
+/** \brief Return a thread local fresh name meant to be used to name local constants. */
+name mk_fresh_local_name();
+expr mk_fresh_local(expr const & type, binder_info const & bi = binder_info());
+/** \brief Return true iff the given constant name is marked as reducible in env() */
+bool is_reducible(name const & n);
+/** \brief Return a nonnull projection_info object if \c n is the name of a projection in env() */
+projection_info const * get_projection_info(name const & n);
+/** \brief Put the given expression in weak-head-normal-form with respect to the
+    current state being processed by the blast tactic. */
+expr whnf(expr const & e);
+/** \brief Return the type of the given expression with respect to the current state being
+    processed by the blast tactic.
+
+    \remark: (potential side-effect) this procedure may update the meta-variable assignment
+    associated with the current state. */
+expr infer_type(expr const & e);
+/** \brief Return true if \c e is a Proposition */
+bool is_prop(expr const & e);
+/** \brief Return true iff the two expressions are definitionally equal in the
+    current state being processed by the blast tactic.
+
+    \remark: (potential side-effect) this procedure may update the meta-variable assignment
+    associated with the current state. */
+bool is_def_eq(expr const & e1, expr const & e2);
+/** \brief Try to synthesize an element of the given type class with respect to the blast local context. */
+optional<expr> mk_class_instance(expr const & e);
+
+/** \brief Display the current state of the blast tactic in the diagnostic channel. */
+void display_curr_state();
+/** \brief Display message in the blast tactic diagnostic channel. */
+void display(char const * msg);
+void display(sstream const & msg);
+/**
+    \brief Create a local scope for saving the assignment and
+    metavariable declarations at curr_state() */
+class scope {
+    bool m_keep;
+public:
+    scope();
+    ~scope();
+    void commit();
+};
+}
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g);
 void initialize_blast();
diff --git a/src/library/blast/blast_context.h b/src/library/blast/blast_context.h
deleted file mode 100644
index e7e241b91f..0000000000
--- a/src/library/blast/blast_context.h
+++ /dev/null
@@ -1,39 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-
-API for accessing the thread local context used by the blast tactic.
-These procedures can only be invoked while the blast tactic is being executed.
-
-Remark: the API is implemented in the file blast.cpp
-*/
-#pragma once
-#include "util/sstream.h"
-#include "library/projection.h"
-#include "library/blast/state.h"
-
-namespace lean {
-namespace blast {
-/** \brief Return the thread local environment being used by the blast tactic. */
-environment const & env();
-/** \brief Return the thread local io_state being used by the blast tactic. */
-io_state const & ios();
-/** \brief Return the thread local current state begin processed by the blast tactic. */
-state & curr_state();
-/** \brief Return the thead local extension context associated with the blast tactic. */
-extension_context & ext_ctx();
-/** \brief Return a thread local fresh name meant to be used to name local constants. */
-name mk_fresh_local_name();
-/** \brief Return true iff the given constant name is marked as reducible in env() */
-bool is_reducible(name const & n);
-/** \brief Return a nonnull projection_info object if \c n is the name of a projection in env() */
-projection_info const * get_projection_info(name const & n);
-
-/** \brief Display the current state of the blast tactic in the diagnostic channel. */
-void display_curr_state();
-/** \brief Display message in the blast tactic diagnostic channel. */
-void display(char const * msg);
-void display(sstream const & msg);
-}}
diff --git a/src/library/blast/infer_type.cpp b/src/library/blast/infer_type.cpp
deleted file mode 100644
index 31fc1e6acb..0000000000
--- a/src/library/blast/infer_type.cpp
+++ /dev/null
@@ -1,534 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/interrupt.h"
-#include "kernel/instantiate.h"
-#include "kernel/abstract.h"
-#include "kernel/for_each_fn.h"
-#include "library/normalize.h"
-#include "library/blast/infer_type.h"
-#include "library/blast/blast_context.h"
-#include "library/blast/blast_exception.h"
-
-namespace lean {
-namespace blast {
-static optional<expr> expand_macro(expr const & m) {
-    lean_assert(is_macro(m));
-    return macro_def(m).expand(m, ext_ctx());
-}
-
-static optional<expr> reduce_projection(expr const & e) {
-    expr const & f = get_app_fn(e);
-    if (!is_constant(f))
-        return none_expr();
-    projection_info const * info = get_projection_info(const_name(f));
-    if (!info)
-        return none_expr();
-    buffer<expr> args;
-    get_app_args(e, args);
-    if (args.size() <= info->m_nparams)
-        return none_expr();
-    unsigned mkidx  = info->m_nparams;
-    expr const & mk = args[mkidx];
-    expr new_mk     = whnf(mk);
-    expr const & new_mk_fn = get_app_fn(new_mk);
-    if (!is_constant(new_mk_fn) || const_name(new_mk_fn) != info->m_constructor)
-        return none_expr();
-    buffer<expr> mk_args;
-    get_app_args(new_mk, mk_args);
-    unsigned i = info->m_nparams + info->m_i;
-    if (i >= mk_args.size())
-        none_expr();
-    expr r = mk_args[i];
-    r = blast::mk_app(r, args.size() - mkidx - 1, args.data() + mkidx + 1);
-    return some_expr(r);
-}
-
-static optional<expr> norm_ext(expr const & e) {
-    if (auto r = reduce_projection(e)) {
-        return r;
-    } else if (auto r = env().norm_ext()(e, ext_ctx())) {
-        return some_expr(r->first);
-    } else {
-        return none_expr();
-    }
-}
-
-static expr whnf_core(expr const & e) {
-    check_system("whnf");
-
-    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::Lambda:
-        return e;
-    case expr_kind::Constant:
-        if (blast::is_reducible(const_name(e)))
-            return whnf_core(instantiate_value_univ_params(env().get(const_name(e)), const_levels(e)));
-        else
-            return e;
-    case expr_kind::Macro:
-        if (auto m = expand_macro(e))
-            return whnf_core(*m);
-        else
-            return e;
-    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);
-            return whnf_core(blast::mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)),
-                                               num_args - m, args.data()));
-        } else {
-            return f == f0 ? e : whnf_core(blast::mk_rev_app(f, args.size(), args.data()));
-        }
-    }}
-    lean_unreachable();
-}
-
-expr whnf(expr const & e) {
-    expr t = e;
-    while (true) {
-        expr t1 = whnf_core(t);
-        if (auto new_t = norm_ext(t1)) {
-            t  = *new_t;
-        } else {
-            return t1;
-        }
-    }
-}
-
-static expr infer_constant(expr const & e) {
-    declaration d    = env().get(const_name(e));
-    auto const & ps = d.get_univ_params();
-    auto const & ls = const_levels(e);
-    if (length(ps) != length(ls))
-        throw blast_exception("infer type failed, incorrect number of universe levels", e);
-    return instantiate_type_univ_params(d, ls);
-}
-
-static expr infer_macro(expr const & e) {
-    auto def = macro_def(e);
-    bool infer_only = true;
-    // Remark: we are ignoring constraints generated by the macro definition.
-    return def.check_type(e, ext_ctx(), infer_only).first;
-}
-
-static expr infer_lambda(expr e) {
-    buffer<expr> es, ds, ls;
-    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 = blast::mk_local(mk_fresh_local_name(), binding_name(e), d, binding_info(e));
-        ls.push_back(l);
-        e = binding_body(e);
-    }
-    expr t = infer_type(instantiate_rev(e, ls.size(), ls.data()));
-    expr r = abstract_locals(t, ls.size(), ls.data());
-    unsigned i = es.size();
-    while (i > 0) {
-        --i;
-        r = blast::mk_pi(binding_name(es[i]), ds[i], r, binding_info(es[i]));
-    }
-    return r;
-}
-
-/** \brief Make sure \c e is a sort, if it is not throw an exception using \c ref as a reference */
-static void ensure_sort(expr const & e, expr const & ref) {
-    // Remark: for simplicity reasons, we just fail if \c e is not a sort.
-    if (!is_sort(e))
-        throw blast_exception("infer type failed, sort expected", ref);
-}
-
-static expr infer_pi(expr const & e0) {
-    buffer<expr>  ls;
-    buffer<level> us;
-    expr e = e0;
-    while (is_pi(e)) {
-        expr d      = instantiate_rev(binding_domain(e), ls.size(), ls.data());
-        expr d_type = whnf(infer_type(d));
-        ensure_sort(d_type, e0);
-        us.push_back(sort_level(d_type));
-        expr l  = blast::mk_local(mk_fresh_local_name(), binding_name(e), d, binding_info(e));
-        ls.push_back(l);
-        e = binding_body(e);
-    }
-    e = instantiate_rev(e, ls.size(), ls.data());
-    expr e_type = whnf(infer_type(e));
-    ensure_sort(e_type, e0);
-    level r = sort_level(e_type);
-    unsigned i = ls.size();
-    bool imp = env().impredicative();
-    while (i > 0) {
-        --i;
-        r = imp ? blast::mk_imax(us[i], r) : blast::mk_max(us[i], r);
-    }
-    return blast::mk_sort(r);
-}
-
-/** \brief Make sure \c e is a Pi-expression, if it is not throw an exception using \c ref as a reference */
-static void ensure_pi(expr const & e, expr const & ref) {
-    // Remark: for simplicity reasons, we just fail if \c e is not a Pi.
-    if (!is_pi(e))
-        throw blast_exception("infer type failed, Pi expected", ref);
-    // Potential problem: e is of the form (f ...) where f is a constant that is not marked as reducible.
-    // So, whnf does not reduce it, and we fail to detect that e is can be reduced to a Pi-expression.
-}
-
-static expr infer_app(expr const & e) {
-    buffer<expr> args;
-    expr const & f = get_app_args(e, args);
-    expr f_type = infer_type(f);
-    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 = whnf(instantiate_rev(f_type, i-j, args.data()+j));
-            ensure_pi(f_type, e);
-            f_type = binding_body(f_type);
-            j = i;
-        }
-    }
-    return instantiate_rev(f_type, nargs-j, args.data()+j);
-}
-
-expr infer_type(expr const & e) {
-    lean_assert(!is_var(e));
-    lean_assert(closed(e));
-    check_system("infer_type");
-
-    expr r;
-    switch (e.kind()) {
-    case expr_kind::Local:
-        if (is_href(e)) {
-            if (hypothesis const * h = curr_state().get_main_branch().get(e)) {
-                r = h->get_type();
-            } else {
-                throw blast_exception("infer type failed, unknown hypothesis", e);
-            }
-        } else {
-            r = mlocal_type(e);
-        }
-        break;
-    case expr_kind::Meta:
-        if (is_mref(e)) {
-            if (metavar_decl const * d = curr_state().get_metavar_decl(mref_index(e))) {
-                r = d->get_type();
-                break;
-            }
-        }
-        throw blast_exception("infer type failed, invalid occurrence of metavariable", e);
-    case expr_kind::Var:
-        lean_unreachable();  // LCOV_EXCL_LINE
-    case expr_kind::Sort:
-        r = blast::mk_sort(blast::mk_succ(sort_level(e)));
-        break;
-    case expr_kind::Constant:
-        r = infer_constant(e);
-        break;
-    case expr_kind::Macro:
-        r = infer_macro(e);
-        break;
-    case expr_kind::Lambda:
-        r = infer_lambda(e);
-        break;
-    case expr_kind::Pi:
-        r = infer_pi(e);
-        break;
-    case expr_kind::App:
-        r = infer_app(e);
-        break;
-    }
-    // TODO(Leo): cache results if we have performance problems
-    return r;
-}
-
-bool is_prop(expr const & e) {
-    if (env().impredicative()) {
-        expr t   = whnf(infer_type(e));
-        return t == mk_Prop();
-    } else {
-        return false;
-    }
-}
-
-bool is_def_eq(level const & l1, level const & l2) {
-    if (is_equivalent(l1, l2)) {
-        return true;
-    } else {
-        state & s = curr_state();
-        if (is_uref(l1)) {
-            if (s.is_uref_assigned(l1)) {
-                return is_def_eq(*s.get_uref_assignment(l1), l2);
-            } else {
-                s.assign_uref(l1, l2);
-                return true;
-            }
-        }
-        if (is_uref(l2)) {
-            if (s.is_uref_assigned(l2)) {
-                return is_def_eq(l1, *s.get_uref_assignment(l2));
-            } else {
-                s.assign_uref(l2, l1);
-                return true;
-            }
-        }
-        return false;
-    }
-}
-
-bool is_def_eq(levels const & ls1, levels const & ls2) {
-    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)) &&
-            is_def_eq(tail(ls1), tail(ls2));
-    } else {
-        return false;
-    }
-}
-
-static bool is_def_eq_core(expr const & e1, expr const & e2);
-
-/** \brief Given \c e of the form <tt>?m t_1 ... t_n</tt>, where
-    ?m is an assigned mref, substitute \c ?m with its assignment. */
-static expr subst_mref(expr const & e) {
-    buffer<expr> args;
-    expr const & u = get_app_args(e, args);
-    expr const * v = curr_state().get_mref_assignment(u);
-    lean_assert(v);
-    return apply_beta(*v, args.size(), args.data());
-}
-
-/** \brief Given \c ma of the form <tt>?m t_1 ... t_n</tt>, (try to) assign
-    ?m to (an abstraction of) v. Return true if success and false otherwise. */
-static bool assign_mref_core(expr const & ma, expr const & v) {
-    buffer<expr> args;
-    expr const & m = get_app_args(ma, args);
-    buffer<expr> locals;
-    for (expr const & arg : args) {
-        if (!blast::is_local(arg))
-            break; // is not local
-        if (std::any_of(locals.begin(), locals.end(), [&](expr const & local) { return local_index(local) == local_index(arg); }))
-            break; // duplicate local
-        locals.push_back(arg);
-    }
-    lean_assert(is_mref(m));
-    state & s = curr_state();
-    metavar_decl const * d = s.get_metavar_decl(m);
-    lean_assert(d);
-    expr new_v = s.instantiate_urefs_mrefs(v);
-    // We must check
-    //   1. All href in new_v are in the context of m.
-    //   2. The context of any (unassigned) mref in new_v must be a subset of the context of m.
-    //      If it is not we force it to be.
-    //   3. Any local constant occurring in new_v occurs in locals
-    //   4. m does not occur in new_v
-    bool ok = true;
-    for_each(new_v, [&](expr const & e, unsigned) {
-            if (!ok)
-                return false; // stop search
-            if (is_href(e)) {
-                if (!d->contains_href(e)) {
-                    ok = false; // failed 1
-                    return false;
-                }
-            } else if (blast::is_local(e)) {
-                if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) { return local_index(a) != local_index(e); })) {
-                    ok = false; // failed 3
-                    return false;
-                }
-            } else if (is_mref(e)) {
-                if (m == e) {
-                    ok = false; // failed 4
-                    return false;
-                }
-                s.restrict_mref_context_using(e, m); // enforce 2
-                return false;
-            }
-            return true;
-        });
-    if (!ok)
-        return false;
-    if (args.empty()) {
-        // easy case
-        s.assign_mref(m, new_v);
-        return true;
-    } else if (args.size() == locals.size()) {
-        s.assign_mref(m, Fun(locals, new_v));
-        return true;
-    } else {
-        // This case is imprecise since it is not a higher order pattern.
-        // That the term \c ma is of the form (?m t_1 ... t_n) and the t_i's are not pairwise
-        // distinct local constants.
-        expr m_type = d->get_type();
-        for (unsigned i = 0; i < args.size(); i++) {
-            m_type = whnf(m_type);
-            if (!is_pi(m_type))
-                return false;
-            lean_assert(i <= locals.size());
-            if (i == locals.size())
-                locals.push_back(blast::mk_local(mk_fresh_local_name(), binding_name(m_type), binding_domain(m_type), binding_info(m_type)));
-            lean_assert(i < locals.size());
-            m_type = instantiate(binding_body(m_type), locals[i]);
-        }
-        lean_assert(locals.size() == args.size());
-        s.assign_mref(m, Fun(locals, new_v));
-        return true;
-    }
-}
-
-/** \brief Given \c ma of the form <tt>?m t_1 ... t_n</tt>, (try to) assign
-    ?m to (an abstraction of) v. Return true if success and false otherwise. */
-static bool assign_mref(expr const & ma, expr const & v) {
-    if (assign_mref_core(ma, v))
-        return true;
-    expr const & f = get_app_fn(v);
-    if (is_mref(f) && curr_state().is_mref_assigned(f))
-        return assign_mref_core(v, ma);
-    return false;
-}
-
-static bool is_def_eq_binding(expr e1, expr e2) {
-    lean_assert(e1.kind() == e2.kind());
-    lean_assert(is_binding(e1));
-    expr_kind k = e1.kind();
-    buffer<expr> subst;
-    do {
-        optional<expr> var_e1_type;
-        if (binding_domain(e1) != binding_domain(e2)) {
-            var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data());
-            expr var_e2_type = instantiate_rev(binding_domain(e2), subst.size(), subst.data());
-            if (!is_def_eq_core(var_e2_type, *var_e1_type))
-                return false;
-        }
-        if (!closed(binding_body(e1)) || !closed(binding_body(e2))) {
-            // local is used inside t or s
-            if (!var_e1_type)
-                var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data());
-            subst.push_back(blast::mk_local(mk_fresh_local_name(), binding_name(e1),
-                                            *var_e1_type, binding_info(e1)));
-        } else {
-            expr const & dont_care = mk_Prop();
-            subst.push_back(dont_care);
-        }
-        e1 = binding_body(e1);
-        e2 = binding_body(e2);
-    } while (e1.kind() == k && e2.kind() == k);
-    return is_def_eq_core(instantiate_rev(e1, subst.size(), subst.data()),
-                          instantiate_rev(e2, subst.size(), subst.data()));
-}
-
-static bool is_def_eq_app(expr const & e1, expr const & e2) {
-    lean_assert(is_app(e1) && is_app(e2));
-    buffer<expr> args1, args2;
-    expr const & f1 = get_app_args(e1, args1);
-    expr const & f2 = get_app_args(e2, args2);
-    if (args1.size() != args2.size() || !is_def_eq_core(f1, f2))
-        return false;
-    for (unsigned i = 0; i < args1.size(); i++) {
-        if (!is_def_eq_core(args1[i], args2[i]))
-            return false;
-    }
-    return true;
-}
-
-static bool is_def_eq_eta(expr const & e1, expr const & e2) {
-    expr new_e1 = try_eta(e1);
-    expr new_e2 = try_eta(e2);
-    if (e1 != new_e1 || e2 != new_e2)
-        return is_def_eq_core(new_e1, new_e2);
-    return false;
-}
-
-static bool is_def_eq_proof_irrel(expr const & e1, expr const & e2) {
-    if (!env().prop_proof_irrel())
-        return false;
-    expr e1_type = infer_type(e1);
-    expr e2_type = infer_type(e2);
-    return is_prop(e1_type) && is_def_eq_core(e1_type, e2_type);
-}
-
-static bool is_def_eq_core(expr const & e1, expr const & e2) {
-    check_system("is_def_eq");
-    if (e1 == e2)
-        return true;
-    expr const & f1 = get_app_fn(e1);
-    if (is_mref(f1)) {
-        if (curr_state().is_mref_assigned(f1)) {
-            return is_def_eq_core(subst_mref(e1), e2);
-        } else {
-            return assign_mref(e1, e2);
-        }
-    }
-    expr const & f2 = get_app_fn(e2);
-    if (is_mref(f2)) {
-        if (curr_state().is_mref_assigned(f2)) {
-            return is_def_eq_core(e1, subst_mref(e2));
-        } else {
-            return assign_mref(e2, e1);
-        }
-    }
-    expr e1_n = whnf(e1);
-    expr e2_n = whnf(e2);
-    if (e1 != e1_n || e2 != e2_n)
-        return is_def_eq_core(e1_n, e2_n);
-    if (e1.kind() == e2.kind()) {
-        switch (e1.kind()) {
-        case expr_kind::Lambda:
-        case expr_kind::Pi:
-            if (is_def_eq_binding(e1, e2))
-                return true;
-            break;
-        case expr_kind::Sort:
-            if (is_def_eq(sort_level(e1), sort_level(e2)))
-                return true;
-            break;
-        case expr_kind::Meta:
-        case expr_kind::Var:
-            lean_unreachable(); // LCOV_EXCL_LINE
-        case expr_kind::Local:
-        case expr_kind::Macro:
-            break;
-        case expr_kind::Constant:
-            if (const_name(e1) == const_name(e2) &&
-                is_def_eq(const_levels(e1), const_levels(e2)))
-                return true;
-            break;
-        case expr_kind::App:
-            if (is_def_eq_app(e1, e2))
-                return true;
-            break;
-        }
-    }
-    if (is_def_eq_eta(e1, e2))
-        return true;
-    return is_def_eq_proof_irrel(e1, e2);
-}
-
-/** \remark Precision of is_def_eq can be improved if mrefs and urefs in e1 and e2 are instantiated
-    before we invoke is_def_eq */
-bool is_def_eq(expr const & e1, expr const & e2) {
-    if (e1 == e2)
-        return true; // quick check
-    state & s = curr_state();
-    state::assignment_snapshot saved(s);
-    bool r = is_def_eq_core(e1, e2);
-    if (!r)
-        saved.restore();
-    return r;
-}
-}}
diff --git a/src/library/blast/infer_type.h b/src/library/blast/infer_type.h
deleted file mode 100644
index ea9b3f859d..0000000000
--- a/src/library/blast/infer_type.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-namespace blast {
-/** \brief Put the given expression in weak-head-normal-form with respect to the
-    current state being processed by the blast tactic. */
-expr whnf(expr const & e);
-/** \brief Return the type of the given expression with respect to the current state being
-    processed by the blast tactic.
-
-    \remark: (potential side-effect) this procedure may update the meta-variable assignment
-    associated with the current state. */
-expr infer_type(expr const & e);
-/** \brief Return true if \c e is a Proposition */
-bool is_prop(expr const & e);
-/** \brief Return true iff the two expressions are definitionally equal in the
-    current state being processed by the blast tactic.
-
-    \remark: (potential side-effect) this procedure may update the meta-variable assignment
-    associated with the current state. */
-bool is_def_eq(expr const & e1, expr const & e2);
-bool is_def_eq(level const & l1, level const & l2);
-bool is_def_eq(levels const & l1, levels const & l2);
-}}
diff --git a/src/library/blast/state.h b/src/library/blast/state.h
index 13feda3c6d..b02cf1e29b 100644
--- a/src/library/blast/state.h
+++ b/src/library/blast/state.h
@@ -75,7 +75,6 @@ public:
 
     // u := l
     void assign_uref(level const & u, level const & l) {
-        lean_assert(!is_uref_assigned(u));
         m_uassignment.insert(uref_index(u), l);
     }
 
@@ -116,7 +115,6 @@ public:
 
     // m := e
     void assign_mref(expr const & m, expr const & e) {
-        lean_assert(!is_mref_assigned(m));
         m_eassignment.insert(mref_index(m), e);
     }