diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean
index c771cd27a5..df6bce5d6f 100644
--- a/library/init/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -9,7 +9,7 @@ import init.meta.level init.meta.expr init.meta.environment init.meta.attribute
 import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic
 import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info
 import init.meta.congr_lemma init.meta.match_tactic init.meta.ac_tactics
-import init.meta.backward init.meta.rewrite_tactic init.meta.unfold_tactic
+import init.meta.backward init.meta.rewrite_tactic
 import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance
 import init.meta.simp_tactic init.meta.set_get_option_tactics
 import init.meta.interactive init.meta.converter
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index deb8ff9560..d1c569ce87 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -318,5 +318,29 @@ to_expr q >>= tactic.subst >> try reflexivity
 meta def clear : raw_ident_list → tactic unit :=
 tactic.clear_lst
 
+private meta def dunfold_hyps : list name → location → tactic unit
+| cs []      := skip
+| cs (h::hs) := get_local h >>= dunfold_at cs >> dunfold_hyps cs hs
+
+meta def dunfold : raw_ident_list → location → tactic unit
+| cs [] := tactic.dunfold cs
+| cs hs := dunfold_hyps cs hs
+
+/- TODO(Leo): add support for non-refl lemmas -/
+meta def unfold : raw_ident_list → location → tactic unit :=
+dunfold
+
+private meta def dunfold_hyps_occs : name → occurrences → location → tactic unit
+| c occs []  := skip
+| c occs (h::hs) := get_local h >>= dunfold_core_at occs [c] >> dunfold_hyps_occs c occs hs
+
+meta def dunfold_occs : ident → list nat → location → tactic unit
+| c ps [] := tactic.dunfold_occs_of ps c
+| c ps hs := dunfold_hyps_occs c (occurrences.pos ps) hs
+
+/- TODO(Leo): add support for non-refl lemmas -/
+meta def unfold_occs : ident → list nat → location → tactic unit :=
+dunfold_occs
+
 end interactive
 end tactic
diff --git a/library/init/meta/occurrences.lean b/library/init/meta/occurrences.lean
index 61c3a7f892..c38feda3d5 100644
--- a/library/init/meta/occurrences.lean
+++ b/library/init/meta/occurrences.lean
@@ -25,6 +25,11 @@ inductive occurrences
 
 open occurrences
 
+def occurrences.contains : occurrences → nat → bool
+| all                  p := tt
+| (occurrences.pos ps) p := to_bool (p ∈ ps)
+| (occurrences.neg ps) p := to_bool (p ∉ ps)
+
 instance : inhabited occurrences :=
 ⟨all⟩
 
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 0f332cb58a..bc8ceb4591 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.tactic init.meta.attribute init.meta.constructor_tactic
-import init.meta.relation_tactics
+import init.meta.relation_tactics init.meta.occurrences
 
 open tactic
 
@@ -68,11 +68,15 @@ meta constant simp_lemmas.simplify_core : simp_lemmas → tactic unit → name 
    The resulting expression is definitionally equal to the input. -/
 meta constant simp_lemmas.dsimplify_core (max_steps : nat) (visit_instances : bool) : simp_lemmas → expr → tactic expr
 
+meta def default_max_steps := 10000000
+
 meta def simp_lemmas.dsimplify : simp_lemmas → expr → tactic expr :=
-simp_lemmas.dsimplify_core 1000000 ff
+simp_lemmas.dsimplify_core default_max_steps ff
 
 namespace tactic
 meta constant dsimplify_core
+  {A : Type}
+  (a : A)
   (max_steps       : nat)
   /- If visit_instances = ff, then instance implicit arguments are not visited, but
      tactic will canonize them. -/
@@ -80,19 +84,22 @@ meta constant dsimplify_core
   /- (pre e) is invoked before visiting the children of subterm 'e',
      if it succeeds the result is a new expression that must be definitionally equal to 'e',
      and a flag indicating whether the new children should be visited or not. -/
-  (pre             : expr → tactic (expr × bool))
+  (pre             : A → expr → tactic (A × expr × bool))
   /- (post e) is invoked after visiting the children of subterm 'e',
      if it succeeds the result is a new expression that must be definitionally equal to 'e',
      and a flag indicating whether the new children should be revisited.
      Remark: if (pre e) returns (some (new_e, ff)), then post is not invoked for new_e. -/
-  (post            : expr → tactic (expr × bool))
-  : expr → tactic expr
+  (post            : A → expr → tactic (A × expr × bool))
+  : expr → tactic (A × expr)
 
 meta def dsimplify
   (pre             : expr → tactic (expr × bool))
   (post            : expr → tactic (expr × bool))
   : expr → tactic expr :=
-dsimplify_core 1000000 ff pre post
+λ e, do (a, new_e) ← dsimplify_core () default_max_steps ff
+                       (λ u e, do r ← pre e, return (u, r))
+                       (λ u e, do r ← post e, return (u, r)) e,
+        return new_e
 
 meta constant dunfold_expr_core : transparency → expr → tactic expr
 
@@ -104,6 +111,44 @@ meta constant unfold_projection_core : transparency → expr → tactic expr
 meta def unfold_projection : expr → tactic expr :=
 unfold_projection_core reducible
 
+meta def dunfold_occs_core (m : transparency) (max_steps : nat) (occs : occurrences) (cs : list name) (e : expr) : tactic expr :=
+let unfold (c : nat) (e : expr) : tactic (nat × expr × bool) := do
+  guard (cs^.any e^.is_app_of),
+  new_e ← dunfold_expr_core m e,
+  if occs^.contains c
+  then return (c+1, new_e, tt)
+  else return (c+1, e, tt)
+in do (c, new_e) ← dsimplify_core 1 max_steps tt unfold (λ c e, failed) e,
+      return new_e
+
+meta def dunfold_core (m : transparency) (max_steps : nat) (cs : list name) (e : expr) : tactic expr :=
+let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
+  guard (cs^.any e^.is_app_of),
+  new_e ← dunfold_expr_core m e,
+  return (u, new_e, tt)
+in do (c, new_e) ← dsimplify_core () max_steps tt (λ c e, failed) unfold e,
+      return new_e
+
+meta def dunfold : list name → tactic unit :=
+λ cs, target >>= dunfold_core reducible default_max_steps cs >>= change
+
+meta def dunfold_occs_of (occs : list nat) (c : name) : tactic unit :=
+target >>= dunfold_occs_core reducible default_max_steps (occurrences.pos occs) [c] >>= change
+
+meta def dunfold_core_at (occs : occurrences) (cs : list name) (h : expr) : tactic unit :=
+do num_reverted : ℕ ← revert h,
+   (expr.pi n bi d b : expr) ← target | failed,
+   new_d : expr ← dunfold_occs_core reducible default_max_steps occs cs d,
+   change $ expr.pi n bi new_d b,
+   intron num_reverted
+
+meta def dunfold_at (cs : list name) (h : expr) : tactic unit :=
+do num_reverted : ℕ ← revert h,
+   (expr.pi n bi d b : expr) ← target | failed,
+   new_d : expr ← dunfold_core reducible default_max_steps cs d,
+   change $ expr.pi n bi new_d b,
+   intron num_reverted
+
 meta def simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
 do lemmas       ← simp_lemmas.mk_default,
    new_lemmas   ← lemmas^.append extra_lemmas,
diff --git a/library/init/meta/unfold_tactic.lean b/library/init/meta/unfold_tactic.lean
deleted file mode 100644
index 529ecfb211..0000000000
--- a/library/init/meta/unfold_tactic.lean
+++ /dev/null
@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.meta.relation_tactics init.meta.occurrences
-
-namespace tactic
-/- (rewrite_core m use_instances occs symm H) -/
-meta constant unfold_expr_core : bool → occurrences → list name → expr → tactic expr
-
-meta def unfold_core (force : bool) (occs : occurrences) (ns : list name) : tactic unit :=
-target >>= unfold_expr_core force occs ns >>= change
-
-meta def unfold : list name → tactic unit :=
-unfold_core ff occurrences.all
-
-meta def unfold_occs_of (occs : list nat) (c : name) : tactic unit :=
-unfold_core ff (occurrences.pos occs) [c]
-
-meta def unfold_core_at (force : bool) (occs : occurrences) (ns : list name) (H : expr) : tactic unit :=
-do num_reverted : ℕ ← revert H,
-   (expr.pi n bi d b : expr) ← target | failed,
-   new_H : expr ← unfold_expr_core force occs ns d,
-   change $ expr.pi n bi new_H b,
-   intron num_reverted
-
-meta def unfold_at : list name → expr → tactic unit :=
-unfold_core_at ff occurrences.all
-
-end tactic
diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index e4050aebc6..d4d0889bff 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -237,19 +237,22 @@ dsimplify_fn::dsimplify_fn(type_context & ctx, unsigned max_steps, bool visit_in
 }
 
 class tactic_dsimplify_fn : public dsimplify_core_fn {
+    vm_obj       m_a;
     vm_obj       m_pre;
     vm_obj       m_post;
     tactic_state m_s;
 
     optional<pair<expr, bool>> invoke_fn(vm_obj const & fn, expr const & e) {
         m_s = set_mctx_lctx(m_s, m_ctx.mctx(), m_ctx.lctx());
-        vm_obj r = invoke(fn, to_obj(e), to_obj(m_s));
+        vm_obj r = invoke(fn, m_a, to_obj(e), to_obj(m_s));
         if (optional<tactic_state> new_s = is_tactic_success(r)) {
             m_s = *new_s;
             m_ctx.set_mctx(m_s.mctx());
             vm_obj p   = cfield(r, 0);
-            expr new_e = to_expr(cfield(p, 0));
-            bool flag  = to_bool(cfield(p, 1));
+            m_a        = cfield(p, 0);
+            vm_obj p1  = cfield(p, 1);
+            expr new_e = to_expr(cfield(p1, 0));
+            bool flag  = to_bool(cfield(p1, 1));
             return optional<pair<expr, bool>>(new_e, flag);
         } else {
             return optional<pair<expr, bool>>();
@@ -266,23 +269,27 @@ class tactic_dsimplify_fn : public dsimplify_core_fn {
 
 public:
     tactic_dsimplify_fn(type_context & ctx, unsigned max_steps, bool visit_instances,
-                        vm_obj const & pre, vm_obj const & post):
+                        vm_obj const & a, vm_obj const & pre, vm_obj const & post):
         dsimplify_core_fn(ctx, max_steps, visit_instances),
+        m_a(a),
         m_pre(pre),
         m_post(post),
         m_s(mk_tactic_state_for(ctx.env(), ctx.get_options(), ctx.mctx(), ctx.lctx(), mk_true())) {
     }
+
+    vm_obj const & get_a() const { return m_a; }
 };
 
-vm_obj tactic_dsimplify_core(vm_obj const & max_steps, vm_obj const & visit_instances,
+vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a,
+                             vm_obj const & max_steps, vm_obj const & visit_instances,
                              vm_obj const & pre, vm_obj const & post, vm_obj const & e, vm_obj const & s) {
     try {
         type_context ctx = mk_type_context_for(to_tactic_state(s));
         tactic_dsimplify_fn F(ctx, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
-                              to_bool(visit_instances), pre, post);
+                              to_bool(visit_instances), a, pre, post);
         expr new_e = F(to_expr(e));
         tactic_state new_s = set_mctx(to_tactic_state(s), F.mctx());
-        return mk_tactic_success(to_obj(new_e), new_s);
+        return mk_tactic_success(mk_vm_pair(F.get_a(), to_obj(new_e)), new_s);
     } catch (exception & ex) {
         return mk_tactic_exception(ex, to_tactic_state(s));
     }
diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp
index 8ff4bd1c0d..6eba526761 100644
--- a/src/library/tactic/unfold_tactic.cpp
+++ b/src/library/tactic/unfold_tactic.cpp
@@ -4,414 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "util/fresh_name.h"
-#include "kernel/abstract.h"
 #include "kernel/instantiate.h"
-#include "kernel/inductive/inductive.h"
-#include "library/util.h"
-#include "library/trace.h"
 #include "library/type_context.h"
-#include "library/replace_visitor.h"
 #include "library/constants.h"
-#include "library/user_recursors.h"
-#include "library/vm/vm_list.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/eqn_lemmas.h"
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/occurrences.h"
 
 namespace lean {
-/* Auxiliary visitor the implements the common parts for unfold_rec_fn and fold_rec_fn. */
-class replace_visitor_aux : public replace_visitor {
-protected:
-    virtual type_context & ctx() = 0;
-
-    expr visit_app_default(expr const & e, expr const & fn, buffer<expr> & args) {
-        bool modified = false;
-        for (expr & arg : args) {
-            expr new_arg = visit(arg);
-            if (arg != new_arg)
-                modified = true;
-            arg = new_arg;
-        }
-        if (!modified)
-            return e;
-        return mk_app(fn, args);
-    }
-
-    virtual expr visit_binding(expr const & b) override {
-        expr new_domain = visit(binding_domain(b));
-        type_context::tmp_locals locals(ctx());
-        expr l          = locals.push_local(binding_name(b), new_domain, binding_info(b));
-        expr new_body   = ctx().abstract_locals(visit(instantiate(binding_body(b), l)), 1, &l);
-        return update_binding(b, new_domain, new_body);
-    }
-};
-
-
-class unfold_rec_fn : public replace_visitor_aux {
-    environment const & m_env;
-    bool                m_force_unfold;
-    type_context &      m_ctx;
-    list<name>          m_to_unfold;
-    occurrences         m_occs;
-    unsigned            m_occ_idx;
-
-    static void throw_ill_formed() {
-        throw exception("ill-formed expression");
-    }
-
-    virtual type_context & ctx() override { return m_ctx; }
-
-    bool is_rec_building_part(name const & n) {
-        if (n == get_prod_fst_name() || n == get_prod_snd_name())
-            return true;
-        if (is_user_defined_recursor(m_env, n))
-            return true;
-        if (n.is_atomic() || !n.is_string())
-            return false;
-        char const * str = n.get_string();
-        return
-            strcmp(str, "rec_on") == 0 ||
-            strcmp(str, "cases_on") == 0 ||
-            strcmp(str, "brec_on") == 0 ||
-            strcmp(str, "below") == 0 ||
-            strcmp(str, "no_confusion") == 0;
-    }
-
-    optional<unsigned> get_local_pos(buffer<expr> const & locals, expr const & e) {
-        if (!is_local(e))
-            return optional<unsigned>();
-        unsigned i = 0;
-        for (expr const & local : locals) {
-            if (mlocal_name(local) == mlocal_name(e))
-                return optional<unsigned>(i);
-            i++;
-        }
-        return optional<unsigned>();
-    }
-
-    /* Return true iff \c e is of the form (C.rec ...) */
-    bool is_rec_app(expr const & e, buffer<expr> const & locals, name & rec_name, buffer<unsigned> & indices_pos,
-                    unsigned & main_arg_pos, buffer<unsigned> & rec_arg_pos) {
-        buffer<expr> args;
-        expr fn = get_app_args(e, args);
-        if (!is_constant(fn))
-            return false;
-        optional<name> I = inductive::is_elim_rule(m_env, const_name(fn));
-        rec_name = const_name(fn);
-        if (!I)
-            return false;
-        if (!is_recursive_datatype(m_env, *I))
-            return false;
-        unsigned major_idx = *inductive::get_elim_major_idx(m_env, const_name(fn));
-        unsigned nindices  = *inductive::get_num_indices(m_env, *I);
-        lean_assert(nindices <= major_idx);
-        unsigned rel_idx   = major_idx - nindices; // first index we should track
-        // Collect position of indices (at least the ones that occur in e)
-        while (rel_idx < args.size() && rel_idx < major_idx) {
-            if (auto it2 = get_local_pos(locals, args[rel_idx])) {
-                indices_pos.push_back(*it2);
-            } else {
-                return false;
-            }
-            rel_idx++;
-        }
-
-        if (major_idx >= args.size()) {
-            // Some indices and the major premise may not occur in e because of eta-reduction
-            main_arg_pos      = locals.size() + major_idx - args.size();
-            for (unsigned i = rel_idx; i < major_idx; i++)
-                indices_pos.push_back(locals.size() + i - args.size());
-            return true;
-        }
-
-        if (auto it = get_local_pos(locals, args[major_idx])) {
-            main_arg_pos = *it;
-        } else {
-            return false;
-        }
-
-        for (unsigned i = major_idx+1; i < args.size(); i++) {
-            if (auto it2 = get_local_pos(locals, args[i])) {
-                rec_arg_pos.push_back(*it2);
-            } else {
-                return false;
-            }
-        }
-        return true;
-    }
-
-    enum rec_kind { BREC, REC, NOREC };
-
-    /* Try to detect the kind of recursive definition */
-    rec_kind get_rec_kind(expr const & e, buffer<expr> const & locals, name & rec_name,
-                          buffer<unsigned> & indices_pos, unsigned & main_arg_pos, buffer<unsigned> & rec_arg_pos) {
-        // tout() << "get_rec_kind: " << e << "\n";
-        if (is_rec_app(e, locals, rec_name, indices_pos, main_arg_pos, rec_arg_pos))
-            return REC;
-        buffer<expr> args;
-        expr fn = get_app_args(e, args);
-        if (is_constant(fn) && const_name(fn) == get_prod_fst_name() &&
-            args.size() >= 3) {
-            // try do detect brec_on pattern
-            if (is_rec_app(args[2], locals, rec_name, indices_pos, main_arg_pos, rec_arg_pos) &&
-                // for brec, eta is not applicable, so main_arg_pos must be < locals.size()
-                main_arg_pos < locals.size()) {
-                for (unsigned i = 3; i < args.size(); i++) {
-                    if (auto it2 = get_local_pos(locals, args[i])) {
-                        rec_arg_pos.push_back(*it2);
-                    } else {
-                        return NOREC;
-                    }
-                }
-                return BREC;
-            }
-        }
-        return NOREC;
-    }
-
-    /* Just unfold the application without trying to fold recursive call */
-    expr unfold_simple(expr const & fn, buffer<expr> & args) {
-        expr new_app = mk_app(fn, args);
-        if (auto r = unfold_term(m_env, new_app)) {
-            return visit(*r);
-        } else {
-            return new_app;
-        }
-    }
-
-    struct fold_failed {};
-
-    struct fold_rec_fn : public replace_visitor_aux {
-        type_context &           m_ctx;
-        expr                     m_fn;    // function being unfolded
-        buffer<expr> const &     m_args;  // arguments of the function being unfolded
-        rec_kind                 m_kind;
-        name                     m_rec_name;
-        unsigned                 m_major_idx; // position of the major premise in the recursor
-        buffer<unsigned> const & m_indices_pos; // position of the datatype indices in the function being unfolded
-        unsigned                 m_main_pos;  // position of the (recursive) argument in the function being unfolded
-        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_context & ctx, 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_ctx(ctx), m_fn(fn), m_args(args), m_kind(k), m_rec_name(rec_name),
-            m_major_idx(*inductive::get_elim_major_idx(m_ctx.env(), rec_name)),
-            m_indices_pos(indices_pos),
-            m_main_pos(main_pos), m_rec_arg_pos(rec_arg_pos) {
-            m_prod_rec_name = inductive::get_elim_name(get_prod_name());
-            lean_assert(m_main_pos < args.size());
-            lean_assert(std::all_of(rec_arg_pos.begin(), rec_arg_pos.end(), [&](unsigned pos) { return pos < args.size(); }));
-        }
-
-        virtual type_context & ctx() override { return m_ctx; }
-
-        expr fold_rec(expr const & e, buffer<expr> const & args) {
-            if (args.size() != m_major_idx + 1 + m_rec_arg_pos.size())
-                throw fold_failed();
-            buffer<expr> new_args;
-            new_args.append(m_args);
-            unsigned nindices = m_indices_pos.size();
-            for (unsigned i = 0; i < m_indices_pos.size(); i++) {
-                new_args[m_indices_pos[i]] = args[m_major_idx - nindices + i];
-            }
-            new_args[m_main_pos] = args[m_major_idx];
-            for (unsigned i = 0; i < m_rec_arg_pos.size(); i++) {
-                new_args[m_rec_arg_pos[i]] = args[m_major_idx + 1 + i];
-            }
-            expr folded_app = mk_app(m_fn, new_args);
-            if (!m_ctx.is_def_eq(folded_app, e))
-                throw fold_failed();
-            return folded_app;
-        }
-
-        expr fold_brec_core(expr const & e, buffer<expr> const & args, unsigned prefix_size, unsigned major_pos) {
-            if (args.size() != prefix_size + m_rec_arg_pos.size()) {
-                throw fold_failed();
-            }
-            buffer<expr> nested_args;
-            get_app_args(args[major_pos], nested_args);
-
-            if (nested_args.size() != m_major_idx+1) {
-                throw fold_failed();
-            }
-            buffer<expr> new_args;
-            new_args.append(m_args);
-            unsigned nindices = m_indices_pos.size();
-            for (unsigned i = 0; i < m_indices_pos.size(); i++) {
-                new_args[m_indices_pos[i]] = nested_args[m_major_idx - nindices + i];
-            }
-            new_args[m_main_pos] = nested_args[m_major_idx];
-            for (unsigned i = 0; i < m_rec_arg_pos.size(); i++) {
-                new_args[m_rec_arg_pos[i]] = args[prefix_size + i];
-            }
-            expr folded_app = mk_app(m_fn, new_args);
-            if (!m_ctx.is_def_eq(folded_app, e))
-                throw fold_failed();
-            return folded_app;
-        }
-
-        expr fold_brec_fst(expr const & e, buffer<expr> const & args) {
-            return fold_brec_core(e, args, 3, 1);
-        }
-
-        expr fold_brec_prod_rec(expr const & e, buffer<expr> const & args) {
-            return fold_brec_core(e, args, 5, 4);
-        }
-
-        virtual expr visit_app(expr const & e) override {
-            buffer<expr> args;
-            expr fn = get_app_args(e, args);
-            if (m_kind == REC && is_constant(fn) && const_name(fn) == m_rec_name) {
-                expr new_e = m_ctx.whnf(e);
-                if (new_e != e)
-                    return visit_app(new_e);
-                else
-                    return fold_rec(e, args);
-            }
-            if (m_kind == BREC && is_constant(fn) && const_name(fn) == get_prod_fst_name() && args.size() >= 3) {
-                expr rec_fn = get_app_fn(args[1]);
-                if (is_constant(rec_fn) && const_name(rec_fn) == m_rec_name)
-                    return fold_brec_fst(e, args);
-            }
-            if (m_kind == BREC && is_constant(fn) && const_name(fn) == m_prod_rec_name && args.size() >= 5) {
-                expr rec_fn = get_app_fn(args[4]);
-                if (is_constant(rec_fn) && const_name(rec_fn) == m_rec_name)
-                    return fold_brec_prod_rec(e, args);
-            }
-            return visit_app_default(e, fn, args);
-        }
-    };
-
-    expr whnf_rec(expr const & e) {
-        return m_ctx.whnf_pred(e, [&](expr const & c) {
-                expr const & fn = get_app_fn(c);
-                return is_constant(fn) && is_rec_building_part(const_name(fn));
-            });
-    }
-
-    expr get_fn_decl(expr const & fn, type_context::tmp_locals & locals) {
-        lean_assert(is_constant(fn));
-        declaration decl = m_env.get(const_name(fn));
-        if (length(const_levels(fn)) != decl.get_num_univ_params())
-            throw_ill_formed();
-        if (!decl.is_definition())
-            throw exception(sstream() << "unfold tactic failed, '" << const_name(fn) << "' is not a definition");
-        expr fn_body     = instantiate_value_univ_params(decl, const_levels(fn));
-        while (is_lambda(fn_body)) {
-            expr local = locals.push_local_from_binding(fn_body);
-            fn_body    = instantiate(binding_body(fn_body), local);
-        }
-        return whnf_rec(fn_body);
-    }
-
-    expr unfold(expr const & fn, buffer<expr> args) {
-        type_context::tmp_locals fn_locals(m_ctx);
-        expr fn_body = get_fn_decl(fn, fn_locals);
-        if (args.size() < fn_locals.size()) {
-            // insufficient args
-            return unfold_simple(fn, args);
-        }
-        name rec_name;
-        unsigned main_pos = 0;
-        buffer<unsigned> indices_pos;
-        buffer<unsigned> rec_arg_pos;
-        rec_kind k = get_rec_kind(fn_body, fn_locals.as_buffer(), rec_name, indices_pos, main_pos, rec_arg_pos);
-        if (k == NOREC || main_pos >= args.size()) {
-            // norecursive definition
-            return unfold_simple(fn, args);
-        }
-        unsigned rest = main_pos >= fn_locals.size() ? main_pos+1 : fn_locals.size();
-        for (unsigned i = rest; i < args.size(); i++)
-            rec_arg_pos.push_back(i);
-        expr new_main  = m_ctx.whnf(args[main_pos]);
-        if (!is_constructor_app(m_env, new_main)) {
-            // argument is not a constructor or constraints were generated
-            throw fold_failed();
-        }
-        args[main_pos]      = new_main;
-        expr fn_body_abst   = m_ctx.abstract_locals(fn_body, fn_locals.as_buffer().size(), fn_locals.as_buffer().data());
-        expr new_e          = instantiate_rev(fn_body_abst, fn_locals.as_buffer().size(), args.data());
-        new_e               = mk_app(new_e, args.size() - fn_locals.as_buffer().size(), args.data() + fn_locals.as_buffer().size());
-        new_e               = whnf_rec(new_e);
-        expr const new_head = get_app_fn(new_e);
-        // TODO(Leo): create an option for the following conditions?
-        if (is_constant(new_head) && inductive::is_elim_rule(m_env, const_name(new_head))) {
-            // head is a recursor... so the unfold is probably not generating a nice result...
-            throw fold_failed();
-        }
-        return fold_rec_fn(m_ctx, fn, args, k, rec_name, indices_pos, main_pos, rec_arg_pos)(new_e);
-    }
-
-    bool unfold_cnst(expr const & e) {
-        if (!is_constant(e))
-            return false;
-        if (std::find(m_to_unfold.begin(), m_to_unfold.end(), const_name(e)) == m_to_unfold.end())
-            return false;
-        m_occ_idx++;
-        return m_occs.contains(m_occ_idx);
-    }
-
-    virtual expr visit_app(expr const & e) override {
-        buffer<expr> args;
-        expr fn = get_app_args(e, args);
-        bool modified = false;
-        for (expr & arg : args) {
-            expr new_arg = visit(arg);
-            if (arg != new_arg)
-                modified = true;
-            arg = new_arg;
-        }
-        if (unfold_cnst(fn)) {
-            try {
-                return unfold(fn, args);
-            } catch (fold_failed &) {
-                if (m_force_unfold)
-                    return unfold_simple(fn, args);
-            }
-        }
-        if (!modified) {
-            return e;
-        } else {
-            return mk_app(fn, args);
-        }
-    }
-
-    virtual expr visit_constant(expr const & e) override {
-        if (unfold_cnst(e)) {
-            if (auto r = unfold_term(m_env, e))
-                return *r;
-        }
-        return e;
-    }
-
-public:
-    unfold_rec_fn(type_context & ctx, bool force_unfold, list<name> const & to_unfold, occurrences const & occs):
-        m_env(ctx.env()),
-        m_force_unfold(force_unfold),
-        m_ctx(ctx),
-        m_to_unfold(to_unfold),
-        m_occs(occs),
-        m_occ_idx(0) {}
-
-    expr operator()(expr const & e) {
-        m_occ_idx = 0;
-        return replace_visitor_aux::operator()(e);
-    }
-};
-
-vm_obj tactic_unfold_expr(vm_obj const & force, vm_obj const & occs, vm_obj const & to_unfold, vm_obj const & e, vm_obj const & s) {
-    try {
-        type_context ctx = mk_type_context_for(to_tactic_state(s));
-        expr r = unfold_rec_fn(ctx, to_bool(force), to_list_name(to_unfold), to_occurrences(occs))(to_expr(e));
-        return mk_tactic_success(to_obj(r), to_tactic_state(s));
-    } catch (exception & ex) {
-        return mk_tactic_exception(ex, to_tactic_state(s));
-    }
-}
-
 vm_obj tactic_unfold_projection_core(vm_obj const & m, vm_obj const & _e, vm_obj const & _s) {
     expr const & e = to_expr(_e);
     tactic_state const & s = to_tactic_state(_s);
@@ -436,8 +37,12 @@ vm_obj tactic_dunfold_expr_core(vm_obj const & m, vm_obj const & _e, vm_obj cons
         expr const & fn = get_app_fn(e);
         if (!is_constant(fn))
             return mk_tactic_exception("dunfold_expr failed, expression is not a constant nor a constant application", s);
-        expr new_e;
-        if (has_eqn_lemmas(env, const_name(fn))) {
+        if (is_projection(s.env(), const_name(fn))) {
+            type_context ctx = mk_type_context_for(s, to_transparency_mode(m));
+            if (auto new_e = ctx.reduce_projection(e))
+                return mk_tactic_success(to_obj(*new_e), s);
+            return mk_tactic_exception("dunfold_expr failed, failed to unfold projection", s);
+        } else if (has_eqn_lemmas(env, const_name(fn))) {
             type_context ctx = mk_type_context_for(s, to_transparency_mode(m));
             buffer<simp_lemma> lemmas;
             bool refl_only = true;
@@ -465,7 +70,6 @@ vm_obj tactic_dunfold_expr_core(vm_obj const & m, vm_obj const & _e, vm_obj cons
 }
 
 void initialize_unfold_tactic() {
-    DECLARE_VM_BUILTIN(name({"tactic", "unfold_expr_core"}), tactic_unfold_expr);
     DECLARE_VM_BUILTIN(name({"tactic", "unfold_projection_core"}), tactic_unfold_projection_core);
     DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr_core"}),      tactic_dunfold_expr_core);
 }
diff --git a/tests/lean/run/dunfold3.lean b/tests/lean/run/dunfold3.lean
new file mode 100644
index 0000000000..c7699e2700
--- /dev/null
+++ b/tests/lean/run/dunfold3.lean
@@ -0,0 +1,30 @@
+open tactic
+
+def g : nat → nat := λ x, x + 5
+
+example (a b : nat) (p : nat → Prop) (h : p (g (nat.succ (nat.succ a)))) : p (g (a + 2)) :=
+begin
+  unfold g at h,
+  do { h ← get_local `h >>= infer_type, t ← to_expr `(p (nat.succ (nat.succ a) + 5)), guard (h = t) },
+  unfold add has_add.add bit0 one nat.add,
+  unfold g,
+  do { t ← target, h ← get_local `h >>= infer_type, guard (t = h) },
+  assumption
+end
+
+meta def check_expected (p : pexpr) : tactic unit :=
+do t ← target, ex ← to_expr p, guard (t = ex)
+
+example (a b c : nat) (f : nat → nat → nat) (h : false) : f (g a) (g b) = (g c) :=
+begin
+  unfold_occs g [2],
+  check_expected `(f (g a) (b + 5) = g c),
+  contradiction
+end
+
+example (a b c : nat) (f : nat → nat → nat) (h : false) : f (g a) (g b) = (g c) :=
+begin
+  unfold_occs g [1, 3],
+  check_expected `(f (a + 5) (g b) = c + 5),
+  contradiction
+end
diff --git a/tests/lean/run/unfold_crash.lean b/tests/lean/run/unfold_crash.lean
index e70113e22c..ab00a3ef76 100644
--- a/tests/lean/run/unfold_crash.lean
+++ b/tests/lean/run/unfold_crash.lean
@@ -31,10 +31,10 @@ by do
      cases_using v2 [`m, `h2, `t2],
      trace_state, trace "------",
      -- unfold only the first occurrence (i.e., the one of the form (vappend nil nil)
-     unfold_occs_of [1] `vappend,
+     dunfold_occs_of [1] `vappend,
      trace_state, trace "------",
      mk_const `Sorry >>= apply,
      -- unfold only the first occurrence (i.e., the one of the form (vappend nil (cons ...))
-     unfold_occs_of [1] `vappend,
+     dunfold_occs_of [1] `vappend,
      trace_state, trace "------",
      repeat $ mk_const `Sorry >>= apply
diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean
index d8b40404c6..82fdfa7ad7 100644
--- a/tests/lean/unfold1.lean
+++ b/tests/lean/unfold1.lean
@@ -1,4 +1,3 @@
-exit -- TODO(Leo): enable test again after we add rfl lemma support to type_context
 open tactic
 
 meta definition rewriteH (Hname : name) : tactic unit :=
@@ -9,10 +8,10 @@ example (l : list nat) : list.append l [] = l :=
 by do
   get_local `l >>= λ H, induction_core semireducible H `list.rec_on [`h, `t, `iH],
   --
-  unfold [`list.append],
+  dunfold [`list.append],
   trace_state,
   trace "------",
   reflexivity,
-  unfold [`list.append],
+  dunfold [`list.append],
   trace_state,
   rewriteH `iH
diff --git a/tests/lean/unfold1.lean.expected.out b/tests/lean/unfold1.lean.expected.out
index 6bc210f8e3..56330aa2b1 100644
--- a/tests/lean/unfold1.lean.expected.out
+++ b/tests/lean/unfold1.lean.expected.out
@@ -1 +1,11 @@
-unfold1.lean:1:0: warning: using 'exit' to interrupt Lean
+⊢ list.nil = list.nil
+
+h : ℕ,
+t : list ℕ,
+iH : list.append t list.nil = t
+⊢ list.append (h :: t) list.nil = h :: t
+------
+h : ℕ,
+t : list ℕ,
+iH : list.append t list.nil = t
+⊢ h :: list.append t list.nil = h :: t
diff --git a/tests/lean/unfold_crash.lean b/tests/lean/unfold_crash.lean
index c46021fcb3..456ebd7b03 100644
--- a/tests/lean/unfold_crash.lean
+++ b/tests/lean/unfold_crash.lean
@@ -4,7 +4,10 @@ open nat tactic
 example (a b : nat) : a = succ b → a = b + 1 :=
 by do
   H ← intro `H,
-  try (unfold_at [`nat.succ] H),
-  unfold [`add], dsimp, unfold [`nat.add],
+  try (dunfold_at [`nat.succ] H),
+  dunfold [`add, `has_add.add, `has_one.one, `nat.add, `one],
   trace_state,
+  t ← target,
+  expected ← to_expr `(a = succ b),
+  guard (t = expected),
   assumption
diff --git a/tests/lean/unfold_crash.lean.expected.out b/tests/lean/unfold_crash.lean.expected.out
index 6cb3ed3e76..2e48796691 100644
--- a/tests/lean/unfold_crash.lean.expected.out
+++ b/tests/lean/unfold_crash.lean.expected.out
@@ -1,3 +1,3 @@
 a b : ℕ,
 H : a = succ b
-⊢ a = add._main b 1
+⊢ a = succ b