diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 31987b7644..b31dd7c51b 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -93,6 +93,11 @@ dsimplify_core 1000000 ff pre post
 
 meta constant dunfold_expr : expr → tactic expr
 
+meta constant unfold_projection_core : transparency → expr → tactic expr
+
+meta def unfold_projection : expr → tactic expr :=
+unfold_projection_core reducible
+
 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/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp
index 30078dd9f2..d01b3eb3e4 100644
--- a/src/library/tactic/unfold_tactic.cpp
+++ b/src/library/tactic/unfold_tactic.cpp
@@ -412,6 +412,22 @@ vm_obj tactic_unfold_expr(vm_obj const & force, vm_obj const & occs, vm_obj cons
     }
 }
 
+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);
+    try {
+        expr const & fn = get_app_fn(e);
+        type_context ctx = mk_type_context_for(s, to_transparency_mode(m));
+        if (!is_constant(fn) || !is_projection(s.env(), const_name(fn)))
+            return mk_tactic_exception("unfold projection failed, expression is not a projection application", s);
+        if (auto new_e = ctx.reduce_projection(e))
+            return mk_tactic_success(to_obj(*new_e), s);
+        return mk_tactic_exception("unfold projection failed, failed to unfold", s);
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
 vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & _s) {
     expr const & e = to_expr(_e);
     tactic_state const & s = to_tactic_state(_s);
@@ -441,12 +457,6 @@ vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & _s) {
             buffer<expr> args;
             get_app_args(e, args);
             expr new_e = head_beta_reduce(mk_app(instantiate_value_univ_params(d, const_levels(fn)), args.size(), args.data()));
-            type_context ctx = mk_type_context_for(s);
-            expr const & new_fn = get_app_fn(new_e);
-            if (is_constant(new_fn) && is_projection(env, const_name(new_fn))) {
-                if (auto new_new_e = ctx.reduce_projection(new_e))
-                    new_e = *new_new_e;
-            }
             return mk_tactic_success(to_obj(new_e), s);
         }
     } catch (exception & ex) {
@@ -456,7 +466,8 @@ vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & _s) {
 
 void initialize_unfold_tactic() {
     DECLARE_VM_BUILTIN(name({"tactic", "unfold_expr_core"}), tactic_unfold_expr);
-    DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr"}), tactic_dunfold_expr);
+    DECLARE_VM_BUILTIN(name({"tactic", "unfold_projection_core"}), tactic_unfold_projection_core);
+    DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr"}),           tactic_dunfold_expr);
 }
 
 void finalize_unfold_tactic() {
diff --git a/tests/lean/run/dunfold1.lean b/tests/lean/run/dunfold1.lean
index 3a6a0bf57b..4c5a6aecde 100644
--- a/tests/lean/run/dunfold1.lean
+++ b/tests/lean/run/dunfold1.lean
@@ -2,11 +2,22 @@ open tactic
 
 set_option pp.all true
 
-example (a b : nat) (p : nat → Prop) (h : p (nat.succ (nat.succ a))) : p (a + 2) :=
+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)) :=
 by do
   t ← target,
-  new_t ← dsimplify (λ e, failed) (λ e, do new_e ← dunfold_expr e, trace e, trace "===>", trace new_e, trace "-------", return (new_e, tt)) t,
-  expected ← to_expr `(p (nat.succ (nat.succ a))),
+  new_t ← dsimplify (λ e, failed)
+     (λ e,
+        do { new_e ← unfold_projection e, return (new_e, tt) }
+        <|>
+        do {
+         guard ([`add, `nat.add, `one, `zero, `bit0, `bit1]^.any e^.is_app_of),
+         new_e ← dunfold_expr e, trace e,
+         trace "===>", trace new_e, trace "-------",
+         return (new_e, tt) })
+     t,
+  expected ← to_expr `(p (g (nat.succ (nat.succ a)))),
   guard (new_t = expected),
   trace new_t,
   assumption