diff --git a/src/library/blast/branch.cpp b/src/library/blast/branch.cpp
index 722174624..5dd640635 100644
--- a/src/library/blast/branch.cpp
+++ b/src/library/blast/branch.cpp
@@ -83,6 +83,9 @@ expr branch::add_hypothesis(name const & n, expr const & type, expr const & valu
     m_next++;
     add_deps(new_h, new_hidx);
     m_context.insert(new_hidx, new_h);
+    if (new_h.is_assumption())
+        m_assumption.insert(new_hidx);
+    m_todo.insert(new_hidx);
     return blast::mk_href(new_hidx);
 }
 
diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h
index f7948e727..dbe944930 100644
--- a/src/library/blast/branch.h
+++ b/src/library/blast/branch.h
@@ -22,6 +22,24 @@ class branch {
     friend class state;
     unsigned           m_next;
     context            m_context;
+    // We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint:
+    //   - assumption
+    //   - active
+    //   - todo
+    //
+    // The sets active and todo are disjoint.
+    //
+    // A hypothesis is an "assumption" if it comes from the input goal,
+    // "intros" proof step, or an assumption obtained when applying an elimination step.
+    //
+    // A hypothesis is derived when it is obtained by forward chaining.
+    // A derived hypothesis can be in the to-do or active sets.
+    //
+    // We say a hypothesis is in the to-do set when the blast haven't process it yet.
+    hypothesis_idx_set m_assumption;
+    hypothesis_idx_set m_active;
+    hypothesis_idx_set m_todo;
+
     forward_deps       m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h.
     expr               m_target;
     hypothesis_idx_set m_target_deps;
@@ -30,7 +48,6 @@ class branch {
     void add_forward_dep(unsigned hidx_user, unsigned hidx_provider);
     void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user);
     void add_deps(hypothesis & h_user, unsigned hidx_user);
-
 public:
     branch():m_next(0) {}
 
@@ -56,6 +73,8 @@ public:
     bool target_depends_on(expr const & h) const { return m_target_deps.contains(href_index(h)); }
 
     bool has_mvar(expr const & e) const { return m_mvar_idxs.contains(mref_index(e)); }
+
+    hypothesis_idx_set get_assumptions() const { return m_assumption; }
 };
 
 void initialize_branch();
diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index 1d3bcb369..89da3cb6e 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -14,14 +14,14 @@ Author: Leonardo de Moura
 namespace lean {
 namespace blast {
 bool metavar_decl::restrict_context_using(metavar_decl const & other) {
-    bool modified = false;
-    m_context.for_each([&](unsigned hidx, hypothesis const &) {
-            if (!other.contains_href(hidx)) {
-                modified = true;
-                m_context.erase(hidx);
-            }
+    buffer<unsigned> to_erase;
+    m_assumptions.for_each([&](unsigned hidx) {
+            if (!other.contains_href(hidx))
+                to_erase.push_back(hidx);
         });
-    return modified;
+    for (unsigned hidx : to_erase)
+        m_assumptions.erase(hidx);
+    return !to_erase.empty();
 }
 
 state::state():m_next_uref_index(0), m_next_mref_index(0) {}
@@ -48,35 +48,32 @@ level state::mk_uref() {
     return blast::mk_uref(idx);
 }
 
-expr state::mk_metavar(context const & ctx, expr const & type) {
+expr state::mk_metavar(hypothesis_idx_set const & c, expr const & type) {
     unsigned midx = m_next_mref_index;
     for_each(type, [&](expr const & e, unsigned) {
             if (!has_href(e))
                 return false;
             if (is_href(e)) {
-                lean_assert(ctx.contains(href_index(e)));
+                lean_assert(c.contains(href_index(e)));
                 add_fixed_by(href_index(e), midx);
                 return false;
             }
             return true; // continue search
         });
     m_next_mref_index++;
-    m_metavar_decls.insert(midx, metavar_decl(ctx, type));
+    m_metavar_decls.insert(midx, metavar_decl(c, type));
     return blast::mk_mref(midx);
 }
 
 expr state::mk_metavar(hypothesis_idx_buffer const & b, expr const & type) {
-    context ctx;
-    for (unsigned const & hidx : b) {
-        hypothesis const * h = m_main.get(hidx);
-        lean_assert(h);
-        ctx.insert(hidx, *h);
-    }
+    hypothesis_idx_set ctx;
+    for (unsigned const & hidx : b)
+        ctx.insert(hidx);
     return mk_metavar(ctx, type);
 }
 
 expr state::mk_metavar(expr const & type) {
-    return state::mk_metavar(m_main.m_context, type);
+    return state::mk_metavar(m_main.get_assumptions(), type);
 }
 
 void state::restrict_mref_context_using(expr const & mref1, expr const & mref2) {
@@ -107,7 +104,7 @@ goal state::to_goal(branch const & b) const {
                         metavar_decl const * decl = m_metavar_decls.find(mref_index(e));
                         lean_assert(decl);
                         buffer<expr> ctx;
-                        decl->get_context().for_each([&](unsigned hidx, hypothesis const &) {
+                        decl->get_assumptions().for_each([&](unsigned hidx) {
                                 ctx.push_back(*hidx2local.find(hidx));
                             });
                         expr type     = convert(decl->get_type());
diff --git a/src/library/blast/state.h b/src/library/blast/state.h
index db51e131e..13feda3c6 100644
--- a/src/library/blast/state.h
+++ b/src/library/blast/state.h
@@ -14,20 +14,22 @@ Author: Leonardo de Moura
 namespace lean {
 namespace blast {
 class metavar_decl {
-    context m_context;
-    expr    m_type;
+    // A metavariable can be assigned to a value that contains references only to the assumptions
+    // that were available when the metavariable was defined.
+    hypothesis_idx_set m_assumptions;
+    expr               m_type;
 public:
     metavar_decl() {}
-    metavar_decl(context const & c, expr const & t):
-        m_context(c), m_type(t) {}
-    context get_context() const { return m_context; }
+    metavar_decl(hypothesis_idx_set const & a, expr const & t):
+        m_assumptions(a), m_type(t) {}
     /** \brief Return true iff \c h is in the context of the this metavar declaration */
-    bool contains_href(expr const & h) const { return m_context.contains(href_index(h)); }
-    bool contains_href(unsigned hidx) const { return m_context.contains(hidx); }
+    bool contains_href(unsigned hidx) const { return m_assumptions.contains(hidx); }
+    bool contains_href(expr const & h) const { return contains_href(href_index(h)); }
     expr const & get_type() const { return m_type; }
     /** \brief Make sure the declaration context of this declaration is a subset of \c other.
         \remark Return true iff the context has been modified. */
     bool restrict_context_using(metavar_decl const & other);
+    hypothesis_idx_set get_assumptions() const { return m_assumptions; }
 };
 
 class state {
@@ -89,9 +91,9 @@ public:
     /** \brief Create a new metavariable using the given type and context.
         \pre ctx must be a subset of the hypotheses in the main branch. */
     expr mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type);
-    expr mk_metavar(context const & ctx, expr const & type);
+    expr mk_metavar(hypothesis_idx_set const & ctx, expr const & type);
 /** \brief Create a new metavariable using the given type.
-        The context of this metavariable will be all hypotheses occurring in the main branch. */
+        The context of this metavariable will be all assumption hypotheses occurring in the main branch. */
     expr mk_metavar(expr const & type);
 
     /** \brief Make sure the metavariable declaration context of mref1 is a