diff --git a/doc/changes.md b/doc/changes.md
index 79dbc55413..b77103a208 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -34,7 +34,7 @@ master branch (aka work in progress branch)
    tries to discharge the subgoal by reducing it to `true`.
    Example: `simp {discharger := assumption}`.
 
-* `simp` can be used to unfold projection applications when the argument is a type class instance.
+* `simp` and `dsimp` can be used to unfold projection applications when the argument is a type class instance.
    Example: `simp [has_add.add]` will replace `@has_add.add nat nat.has_add a b` with `nat.add a b`
 
 * `dsimp` has several new configuration options to control reduction (e.g., `iota`, `beta`, `zeta`, ...).
@@ -62,6 +62,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 * `dsimp` does not unfold reducible definitions by default anymore.
   Example: `function.comp` applications will not be unfolded by default.
   We should use `dsimp [f]` if we want to reduce a reducible definition `f`.
+  Another option is to use the new configuration parameter `unfold_reducible`.
+  Example `dsimp {unfold_reducible := tt}`
 
 * All `dunfold` and `unfold` tactics fail if they did not unfold anything.
   We can simulate the v3.2.0 using `unfold f {fail_if_unchaged := ff}` or `try {unfold f}`.
@@ -73,6 +75,18 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
    and it is shorthand for `unfold f {single_pass := tt}`.
    Remark: in v3.2.0, `unfold` was just an alias for the `dunfold` tactic.
 
+*API name changes*
+
+* `tactic.dsimp` and `tactic.dsimp_core` => `tactic.dsimp_target`
+* `tactic.dsimp_at_core` and `tactic.dsimp_at` => `tactic.dsimp_hyp`
+* `tactic.delta_expr` => `tactic.delta`
+* `tactic.delta` => `tactic.delta_target`
+* `tactic.delta_at` => `tactic.delta_hyp`
+* `tactic.simplify_goal` => `tactic.simp_target`
+* `tactic.unfold_projection` => `tactic.unfold_proj`
+* `tactic.unfold_projections_core` => `tactic.unfold_projs`
+* `tactic.unfold_projections` => `tactic.unfold_projs_target`
+* `tactic.unfold_projections_at` => `tactic.unfold_projs_hyp`
 
 v3.2.0 (18 June 2017)
 -------------
diff --git a/library/init/meta/converter/conv.lean b/library/init/meta/converter/conv.lean
index 8448c7cdac..14261d2ee5 100644
--- a/library/init/meta/converter/conv.lean
+++ b/library/init/meta/converter/conv.lean
@@ -67,13 +67,13 @@ reflexivity
 meta def whnf : conv unit :=
 lhs >>= tactic.whnf >>= change
 
-meta def dsimp (s : option simp_lemmas := none) (cfg : dsimp_config := {}) : conv unit :=
+meta def dsimp (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : conv unit :=
 do s ← match s with
        | some s := return s
        | none   := simp_lemmas.mk_default
        end,
    l ← lhs,
-   s.dsimplify l cfg >>= change
+   s.dsimplify u l cfg >>= change
 
 private meta def congr_aux : list congr_arg_kind → list expr → tactic (list expr × list expr)
 | []      []      := return ([], [])
diff --git a/library/init/meta/converter/interactive.lean b/library/init/meta/converter/interactive.lean
index d94d54ec41..27f8e9ffb2 100644
--- a/library/init/meta/converter/interactive.lean
+++ b/library/init/meta/converter/interactive.lean
@@ -42,7 +42,7 @@ conv.whnf
 meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list)
                (ids : parse without_ident_list) (cfg : tactic.dsimp_config := {}) : conv unit :=
 do (s, u) ← tactic.mk_simp_set no_dflt attr_names es ids,
-   conv.dsimp (some s) cfg
+   conv.dsimp (some s) u cfg
 
 meta def trace_lhs : conv unit :=
 lhs >>= tactic.trace
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index b35ad85bf5..8a5ff9b6cd 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -813,18 +813,18 @@ do (s, u) ← mk_simp_set no_dflt attr_names hs wo_ids,
    end,
    try triv >> try (reflexivity reducible)
 
-private meta def dsimp_hyps (s : simp_lemmas) (hs : list name) (cfg : dsimp_config := {}) : tactic unit :=
-hs.mfor' (λ h_name, do h ← get_local h_name, dsimp_at_core s h cfg)
+private meta def dsimp_hyps (s : simp_lemmas) (u : list name) (hs : list name) (cfg : dsimp_config := {}) : tactic unit :=
+hs.mfor' (λ h_name, do h ← get_local h_name, dsimp_hyp h s u cfg)
 
 meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list)
                (ids : parse without_ident_list) (l : parse location) (cfg : dsimp_config := {}) : tactic unit :=
 match l with
-| (loc.ns [])    := do (s, u) ← mk_simp_set no_dflt attr_names es ids, tactic.dsimp_core s cfg
-| (loc.ns hs)    := do (s, u) ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s hs cfg
+| (loc.ns [])    := do (s, u) ← mk_simp_set no_dflt attr_names es ids, dsimp_target s u cfg
+| (loc.ns hs)    := do (s, u) ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s u hs cfg
 | (loc.wildcard) := do ls ← local_context,
                        n ← revert_lst ls,
                        (s, u) ← mk_simp_set no_dflt attr_names es ids,
-                       tactic.dsimp_core s cfg,
+                       dsimp_target s u cfg,
                        intron n
 end
 
@@ -904,28 +904,28 @@ end
 
 private meta def delta_hyps : list name → list name → tactic unit
 | cs []      := skip
-| cs (h::hs) := get_local h >>= delta_at cs >> delta_hyps cs hs
+| cs (h::hs) := get_local h >>= delta_hyp cs >> delta_hyps cs hs
 
 meta def delta : parse ident* → parse location → tactic unit
-| cs (loc.ns [])    := do new_cs ← to_qualified_names cs, tactic.delta new_cs
+| cs (loc.ns [])    := do new_cs ← to_qualified_names cs, delta_target new_cs
 | cs (loc.ns hs)    := do new_cs ← to_qualified_names cs, delta_hyps new_cs hs
 | cs (loc.wildcard) := do ls ← tactic.local_context,
                           n ← revert_lst ls,
                           new_cs ← to_qualified_names cs,
-                          tactic.delta new_cs,
+                          delta_target new_cs,
                           intron n
 
-private meta def unfold_projections_hyps : list name → tactic unit
+private meta def unfold_projs_hyps : list name → tactic unit
 | []      := skip
-| (h::hs) := get_local h >>= unfold_projections_at >> unfold_projections_hyps hs
+| (h::hs) := get_local h >>= unfold_projs_hyp >> unfold_projs_hyps hs
 
 /--
 This tactic unfolds all structure projections.
 -/
-meta def unfold_projections : parse location → tactic unit
-| (loc.ns [])    := tactic.unfold_projections
-| (loc.ns hs)    := unfold_projections_hyps hs
-| (loc.wildcard) := do ls ← local_context, unfold_projections_hyps (ls.map expr.local_pp_name)
+meta def unfold_projs : parse location → tactic unit
+| (loc.ns [])    := tactic.unfold_projs_target
+| (loc.ns hs)    := unfold_projs_hyps hs
+| (loc.wildcard) := do ls ← local_context, unfold_projs_hyps (ls.map expr.local_pp_name)
 
 end interactive
 
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 175ee6ed3b..9f4e8e0105 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -73,12 +73,15 @@ structure dsimp_config :=
 (beta : bool               := tt)
 (proj : bool               := tt) -- reduce projections
 (iota : bool               := tt)
+(unfold_reducible          := ff) -- if tt, reducible definitions will be unfolded (delta-reduced)
 (memoize                   := tt)
 end tactic
 
 /-- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
-   The resulting expression is definitionally equal to the input. -/
-meta constant simp_lemmas.dsimplify (s : simp_lemmas) (e : expr) (cfg : tactic.dsimp_config := {}) : tactic expr
+   The resulting expression is definitionally equal to the input.
+
+   The list `u` contains defintions to be delta-reduced, and projections to be reduced.-/
+meta constant simp_lemmas.dsimplify (s : simp_lemmas) (u : list name := []) (e : expr) (cfg : tactic.dsimp_config := {}) : tactic expr
 
 namespace tactic
 /- Remark: the configuration parameters `cfg.md` and `cfg.eta` are ignored by this tactic. -/
@@ -110,18 +113,15 @@ meta def dsimplify
                        (λ u e, do r ← post e, return (u, r)) e,
         return new_e
 
-meta def dsimp_core (s : simp_lemmas) (cfg : dsimp_config := {}) : tactic unit :=
-do t ← target, s.dsimplify t cfg >>= unsafe_change
+meta def get_simp_lemmas_or_default : option simp_lemmas → tactic simp_lemmas
+| none     := simp_lemmas.mk_default
+| (some s) := return s
 
-meta def dsimp (cfg : dsimp_config := {}) : tactic unit :=
-do s ← simp_lemmas.mk_default, dsimp_core s cfg
-
-meta def dsimp_at_core (s : simp_lemmas) (h : expr) (cfg : dsimp_config := {}) : tactic unit :=
-revert_and_transform (λ e, s.dsimplify e cfg) h
-
-meta def dsimp_at (h : expr) (cfg : dsimp_config := {}) : tactic unit :=
-do s ← simp_lemmas.mk_default, dsimp_at_core s h cfg
+meta def dsimp_target (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : tactic unit :=
+do s ← get_simp_lemmas_or_default s, t ← target, s.dsimplify u t cfg >>= unsafe_change
 
+meta def dsimp_hyp (h : expr) (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : tactic unit :=
+do s ← get_simp_lemmas_or_default s, revert_and_transform (λ e, s.dsimplify u e cfg) h
 
 /- Remark: we use transparency.instances by default to make sure that we
    can unfold projections of type classes. Example:
@@ -130,8 +130,6 @@ do s ← simp_lemmas.mk_default, dsimp_at_core s h cfg
 -/
 
 /-- If `e` is a projection application, try to unfold it, otherwise fail. -/
-meta constant unfold_projection (e : expr) (md := transparency.instances) : tactic expr
-
 meta constant dunfold_expr (e : expr) (md := transparency.instances) : tactic expr
 
 structure dunfold_config extends dsimp_config :=
@@ -157,7 +155,7 @@ cs.any (λ c,
        f.is_constant && f.const_name.is_internal && (f.const_name.get_prefix = c))
 
 /-- Delta reduce the given constant names -/
-meta def delta_expr (cs : list name) (e : expr) (cfg : delta_config) : tactic expr :=
+meta def delta (cs : list name) (e : expr) (cfg : delta_config := {}) : tactic expr :=
 let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
   guard (is_delta_target e cs),
   (expr.const f_name f_lvls) ← return e.get_app_fn,
@@ -169,24 +167,29 @@ let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
 in do (c, new_e) ← dsimplify_core () (λ c e, failed) unfold e {max_steps := cfg.max_steps, canonize_instances := cfg.visit_instances},
       return new_e
 
-meta def delta (cs : list name) : tactic unit :=
-do t ← target, delta_expr cs t {} >>= unsafe_change
+meta def delta_target (cs : list name) (cfg : delta_config := {}) : tactic unit :=
+do t ← target, delta cs t cfg >>= unsafe_change
 
-meta def delta_at (cs : list name) : expr → tactic unit :=
-revert_and_transform (λ e, delta_expr cs e {})
+meta def delta_hyp (cs : list name) (h : expr) (cfg : delta_config := {}) :tactic unit :=
+revert_and_transform (λ e, delta cs e cfg) h
 
-meta def unfold_projections_core (e : expr) (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic expr :=
+structure unfold_proj_config extends dsimp_config :=
+(md := transparency.instances)
+
+meta constant unfold_proj (e : expr) (md := transparency.instances) : tactic expr
+
+meta def unfold_projs (e : expr) (cfg : unfold_proj_config := {}) : tactic expr :=
 let unfold (changed : bool) (e : expr) : tactic (bool × expr × bool) := do
-  new_e ← unfold_projection e md,
+  new_e ← unfold_proj e cfg.md,
   return (tt, new_e, tt)
-in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e {max_steps := max_steps, md := md} | fail "no projections to unfold",
+in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e cfg.to_dsimp_config | fail "no projections to unfold",
       return new_e
 
-meta def unfold_projections (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic unit :=
-do t ← target, unfold_projections_core t md max_steps >>= unsafe_change
+meta def unfold_projs_target (cfg : unfold_proj_config := {}) : tactic unit :=
+do t ← target, unfold_projs t cfg >>= unsafe_change
 
-meta def unfold_projections_at (h : expr) (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic unit :=
-revert_and_transform (λ e, unfold_projections_core e md max_steps) h
+meta def unfold_projs_hyp (h : expr) (cfg : unfold_proj_config := {}) : tactic unit :=
+revert_and_transform (λ e, unfold_projs e cfg) h
 
 structure simp_config :=
 (max_steps : nat           := simp.default_max_steps)
@@ -215,7 +218,7 @@ structure simp_config :=
 meta constant simplify (s : simp_lemmas) (to_unfold : list name) (e : expr) (cfg : simp_config := {}) (r : name := `eq)
                        (discharger : tactic unit := failed) : tactic (expr × expr)
 
-meta def simplify_goal (S : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic unit :=
+meta def simp_target (S : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic unit :=
 do t ← target,
    (new_t, pr) ← simplify S to_unfold t cfg `eq discharger,
    replace_target new_t pr
@@ -274,7 +277,7 @@ meta def intro1_aux : bool → list name → tactic expr
 | _  _       := failed
 
 meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool → list name → tactic simp_lemmas
-| S tt     [] := try (simplify_goal S [] cfg) >> return S
+| S tt     [] := try (simp_target S [] cfg) >> return S
 | S use_ns ns := do
   t ← target,
   if t.is_napp_of `not 1 then
@@ -301,7 +304,7 @@ meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool
     new_t ← whnf t reducible,
     if new_t.is_pi then unsafe_change new_t >> simp_intro_aux S use_ns ns
     else
-      try (simplify_goal S [] cfg) >>
+      try (simp_target S [] cfg) >>
       mcond (expr.is_pi <$> target)
         (simp_intro_aux S use_ns ns)
         (if use_ns ∧ ¬ns.empty then failed else return S)
@@ -423,7 +426,6 @@ do
   let s := remove_deps s t,
   return $ ctx.filter (λ h, s.contains h.local_uniq_name)
 
-
 section simp_all
 
 meta structure simp_all_entry :=
@@ -471,7 +473,7 @@ private meta def loop (cfg : simp_config) (discharger : tactic unit) (to_unfold
   if m then loop r [] s ff
   else do
     add_new_hyps r,
-    target_changed ← (simplify_goal s to_unfold cfg discharger >> return tt) <|> return ff,
+    target_changed ← (simp_target s to_unfold cfg discharger >> return tt) <|> return ff,
     guard (cfg.fail_if_unchanged = ff ∨ target_changed ∨ r.any (λ e, e.pr ≠ none)) <|> fail "simp_all tactic failed to simplify",
     clear_old_hyps r
 | (e::es) r  s m := do
diff --git a/library/init/meta/well_founded_tactics.lean b/library/init/meta/well_founded_tactics.lean
index 3310891e76..7f8e0391fa 100644
--- a/library/init/meta/well_founded_tactics.lean
+++ b/library/init/meta/well_founded_tactics.lean
@@ -79,7 +79,7 @@ private meta def unfold_sizeof_loop : tactic unit :=
 do
   dunfold [``sizeof, ``has_sizeof.sizeof] {fail_if_unchanged := ff},
   S ← target >>= collect_sizeof_lemmas,
-  (simplify_goal S >> unfold_sizeof_loop)
+  (simp_target S >> unfold_sizeof_loop)
   <|>
   try `[simp]
 
diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index c411d31e23..a896ce525b 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -12,8 +12,10 @@ Author: Leonardo de Moura
 #include "library/fun_info.h"
 #include "library/util.h"
 #include "library/trace.h"
+#include "library/reducible.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_nat.h"
+#include "library/vm/vm_list.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/dsimplify.h"
 #include "library/tactic/simp_lemmas.h"
@@ -58,6 +60,26 @@ expr reduce_beta_eta_proj_iota(type_context & ctx, expr e, bool beta, bool eta,
     return e;
 }
 
+optional<expr> unfold_step(type_context & ctx, expr const & e, name_set const & to_unfold, bool unfold_reducible) {
+    if (!unfold_reducible && to_unfold.empty())
+        return none_expr();
+    if (!is_app(e) && !is_constant(e))
+        return none_expr();
+    expr const & fn = get_app_fn(e);
+    if (!is_constant(fn))
+        return none_expr();
+    name const & fn_name = const_name(fn);
+    if (!to_unfold.contains(const_name(fn)) && (!unfold_reducible || !is_reducible(ctx.env(), fn_name)))
+        return none_expr();
+    type_context::transparency_scope scope(ctx, transparency_mode::Instances);
+    optional<expr> new_e;
+    if (is_projection(ctx.env(), const_name(fn))) {
+        return ctx.reduce_projection(e);
+    } else {
+        return unfold_term(ctx.env(), e);
+    }
+}
+
 dsimp_config::dsimp_config():
     m_md(transparency_mode::Reducible),
     m_max_steps(LEAN_DEFAULT_DSIMPLIFY_MAX_STEPS),
@@ -69,6 +91,7 @@ dsimp_config::dsimp_config():
     m_beta(true),
     m_proj(true),
     m_iota(true),
+    m_unfold_reducible(false),
     m_memoize(true) {
 }
 dsimp_config::dsimp_config(vm_obj const & o) {
@@ -82,7 +105,8 @@ dsimp_config::dsimp_config(vm_obj const & o) {
     m_beta               = to_bool(cfield(o, 7));
     m_proj               = to_bool(cfield(o, 8));
     m_iota               = to_bool(cfield(o, 9));
-    m_memoize            = to_bool(cfield(o, 10));
+    m_unfold_reducible   = to_bool(cfield(o, 10));
+    m_memoize            = to_bool(cfield(o, 11));
 }
 
 #define lean_dsimp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
@@ -294,6 +318,8 @@ optional<pair<expr, bool>> dsimplify_fn::pre(expr const & e) {
 }
 
 optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
+    if (auto r = unfold_step(m_ctx, e, m_to_unfold, m_cfg.m_unfold_reducible))
+        return optional<pair<expr, bool>>(*r, true);
     expr curr_e;
     {
         type_context::transparency_scope s(m_ctx, m_cfg.m_md);
@@ -332,9 +358,11 @@ optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
         return optional<pair<expr, bool>>(curr_e, true);
 }
 
-dsimplify_fn::dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas_for const & lemmas, dsimp_config const & cfg):
+dsimplify_fn::dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas_for const & lemmas,
+                           list<name> const & to_unfold, dsimp_config const & cfg):
     dsimplify_core_fn(ctx, dcs, cfg),
-    m_simp_lemmas(lemmas) {
+    m_simp_lemmas(lemmas),
+    m_to_unfold(to_name_set(to_unfold)) {
 }
 
 class tactic_dsimplify_fn : public dsimplify_core_fn {
@@ -404,16 +432,17 @@ vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a,
     }
 }
 
-vm_obj simp_lemmas_dsimplify(vm_obj const & lemmas, vm_obj const & e, vm_obj const & _cfg, vm_obj const & _s) {
+vm_obj simp_lemmas_dsimplify(vm_obj const & lemmas, vm_obj const & u, vm_obj const & e, vm_obj const & _cfg, vm_obj const & _s) {
     tactic_state const & s = tactic::to_state(_s);
     dsimp_config cfg(_cfg);
     try {
-        type_context ctx    = mk_type_context_for(s, cfg.m_md);
-        defeq_can_state dcs = s.dcs();
+        type_context ctx     = mk_type_context_for(s, cfg.m_md);
+        defeq_can_state dcs  = s.dcs();
+        list<name> to_unfold = to_list_name(u);
         simp_lemmas_for dlemmas;
         if (auto * dls = to_simp_lemmas(lemmas).find(get_eq_name()))
             dlemmas = *dls;
-        dsimplify_fn F(ctx, dcs, dlemmas, cfg);
+        dsimplify_fn F(ctx, dcs, dlemmas, to_unfold, cfg);
         expr new_e = F(to_expr(e));
         if (cfg.m_fail_if_unchanged && to_expr(e) == new_e) {
             return tactic::mk_exception("dsimplify tactic failed to simplify", s);
diff --git a/src/library/tactic/dsimplify.h b/src/library/tactic/dsimplify.h
index 750e8bd844..7521d6e9e0 100644
--- a/src/library/tactic/dsimplify.h
+++ b/src/library/tactic/dsimplify.h
@@ -21,8 +21,9 @@ structure dsimp_config :=
 (eta : bool                := ff)
 (zeta : bool               := ff)
 (beta : bool               := tt)
-(proj : bool               := tt) -- reduce projections
+(proj : bool               := tt)
 (iota : bool               := tt)
+(unfold_reducible          := ff)
 (memoize                   := tt)
 */
 struct dsimp_config {
@@ -36,6 +37,7 @@ struct dsimp_config {
     bool                      m_beta;
     bool                      m_proj;
     bool                      m_iota;
+    bool                      m_unfold_reducible;
     bool                      m_memoize;
     dsimp_config();
     dsimp_config(vm_obj const & o);
@@ -69,15 +71,17 @@ public:
 
 class dsimplify_fn : public dsimplify_core_fn {
     simp_lemmas_for   m_simp_lemmas;
+    name_set          m_to_unfold;
     expr reduce(expr const & e);
     virtual optional<pair<expr, bool>> pre(expr const & e) override;
     virtual optional<pair<expr, bool>> post(expr const & e) override;
 public:
     dsimplify_fn(type_context & ctx, defeq_canonizer::state & s,
-                 simp_lemmas_for const & lemmas, dsimp_config const & cfg);
+                 simp_lemmas_for const & lemmas, list<name> const & to_unfold, dsimp_config const & cfg);
 };
 
 expr reduce_beta_eta_proj_iota(type_context & ctx, expr e, bool beta, bool eta, bool proj, bool iota);
+optional<expr> unfold_step(type_context & ctx, expr const & e, name_set const & to_unfold, bool unfold_reducible);
 
 void initialize_dsimplify();
 void finalize_dsimplify();
diff --git a/src/library/tactic/simp_result.h b/src/library/tactic/simp_result.h
index d1c3adc3ca..e5f5e88386 100644
--- a/src/library/tactic/simp_result.h
+++ b/src/library/tactic/simp_result.h
@@ -41,5 +41,4 @@ simp_result join(type_context & tctx, name const & rel, simp_result const & r1,
 
 simp_result finalize_eq(abstract_type_context & tctx, simp_result const & r);
 simp_result join_eq(abstract_type_context & tctx, simp_result const & r1, simp_result const & r2);
-
 }
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index 38ac324629..9c856ea9f1 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -1050,31 +1050,9 @@ optional<pair<simp_result, bool>> simplify_fn::pre(expr const &, optional<expr>
     return no_ext_result();
 }
 
-static optional<simp_result> to_opt_simp_result(optional<expr> const & e) {
-    if (!e) return optional<simp_result>();
-    return optional<simp_result>(*e);
-}
-
-optional<simp_result> simplify_fn::unfold_step(expr const & e) {
-    if (m_to_unfold.empty())
-        return optional<simp_result>();
-    if (!is_app(e) && !is_constant(e))
-        return optional<simp_result>();
-    expr const & fn = get_app_fn(e);
-    if (!is_constant(fn) || !m_to_unfold.contains(const_name(fn)))
-        return optional<simp_result>();
-    type_context::transparency_scope scope(m_ctx, transparency_mode::Instances);
-    optional<expr> new_e;
-    if (is_projection(m_ctx.env(), const_name(fn))) {
-        return to_opt_simp_result(m_ctx.reduce_projection(e));
-    } else {
-        return to_opt_simp_result(unfold_term(m_ctx.env(), e));
-    }
-}
-
 optional<pair<simp_result, bool>> simplify_fn::post(expr const & e, optional<expr> const &) {
-    if (auto r = unfold_step(e))
-        return to_ext_result(*r);
+    if (auto r = unfold_step(m_ctx, e, m_to_unfold, false))
+        return to_ext_result(simp_result(*r));
     simp_result r = rewrite(e);
     if (r.get_new() != e) {
         return to_ext_result(r);
diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h
index 5e284e4363..9abb6beb9d 100644
--- a/src/library/tactic/simplify.h
+++ b/src/library/tactic/simplify.h
@@ -171,7 +171,6 @@ public:
 class simplify_fn : public simplify_ext_core_fn {
 protected:
     name_set m_to_unfold;
-    optional<simp_result> unfold_step(expr const & e);
     virtual optional<pair<simp_result, bool>> pre(expr const & e, optional<expr> const & parent) override;
     virtual optional<pair<simp_result, bool>> post(expr const & e, optional<expr> const & parent) override;
     virtual optional<expr> prove(expr const & e) override;
diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp
index bdb12b1cf4..ed5d5dd75b 100644
--- a/src/library/tactic/smt/hinst_lemmas.cpp
+++ b/src/library/tactic/smt/hinst_lemmas.cpp
@@ -256,7 +256,7 @@ static expr dsimp(type_context & ctx, transparency_mode md, expr const & e) {
     cfg.m_canonize_instances = false;
     cfg.m_max_steps          = 1000000; /* TODO(Leo): add parameter? */
     cfg.m_eta                = true;
-    return dsimplify_fn(ctx, dcs, simp_lemmas_for(), cfg)(e);
+    return dsimplify_fn(ctx, dcs, simp_lemmas_for(), list<name>(), cfg)(e);
 }
 
 struct mk_hinst_lemma_fn {
diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp
index efda3fa0d4..e5f3d1622f 100644
--- a/src/library/tactic/smt/smt_state.cpp
+++ b/src/library/tactic/smt/smt_state.cpp
@@ -207,7 +207,7 @@ static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_
     simp_lemmas_for eq_lemmas;
     if (auto r = cfg.m_simp_lemmas.find(get_eq_name()))
         eq_lemmas = *r;
-    return dsimplify_fn(ctx, dcs, eq_lemmas, dcfg);
+    return dsimplify_fn(ctx, dcs, eq_lemmas, list<name>(), dcfg);
 }
 
 static simplify_fn mk_simp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) {
diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp
index 1872ffee7b..17c41f8b5b 100644
--- a/src/library/tactic/unfold_tactic.cpp
+++ b/src/library/tactic/unfold_tactic.cpp
@@ -165,7 +165,7 @@ vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & m, vm_obj const & _
 }
 
 void initialize_unfold_tactic() {
-    DECLARE_VM_BUILTIN(name({"tactic", "unfold_projection"}),  tactic_unfold_projection);
+    DECLARE_VM_BUILTIN(name({"tactic", "unfold_proj"}),  tactic_unfold_projection);
     DECLARE_VM_BUILTIN(name({"tactic", "dunfold_core"}),       tactic_dunfold_core);
     DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr"}),       tactic_dunfold_expr);
 }
diff --git a/tests/lean/change1.lean b/tests/lean/change1.lean
index bed5ea272b..db2d87a9d4 100644
--- a/tests/lean/change1.lean
+++ b/tests/lean/change1.lean
@@ -6,10 +6,9 @@ rfl
 
 example (a b : nat) : a = b → succ (succ a) = succ (b + 1) :=
 by do intro `Heq,
-      t  ← target,
       trace_state,
       s ← simp_lemmas.mk_default,
-      t' ← s^.dsimplify t,
+      t' ← target >>= s^.dsimplify,
       change t',
       trace "---- after change ----",
       trace_state,
diff --git a/tests/lean/change2.lean b/tests/lean/change2.lean
index 26ba612c22..c23cb87498 100644
--- a/tests/lean/change2.lean
+++ b/tests/lean/change2.lean
@@ -8,7 +8,7 @@ example (a b : nat) : a = b → succ (succ a) = succ (b + 1) :=
 by do intro `Heq,
       get_local `a >>= subst,
       trace_state,
-      dsimp,
+      dsimp_target,
       trace "---- after dsimp ----",
       trace_state,
       t ← target,
diff --git a/tests/lean/defeq1.lean b/tests/lean/defeq1.lean
index 06b0fd634c..178fb2a044 100644
--- a/tests/lean/defeq1.lean
+++ b/tests/lean/defeq1.lean
@@ -9,6 +9,6 @@ example (n m : nat) (H : succ (succ n) = succ m) : true :=
 by do H  ← get_local `H,
       t  ← infer_type H,
       s  ← simp_lemmas.mk_default,
-      t' ← s^.dsimplify t,
+      t' ← s^.dsimplify [] t,
       trace t',
       exact (expr.const `trivial [])
diff --git a/tests/lean/defeq_simp2.lean b/tests/lean/defeq_simp2.lean
index d04249d3e7..0a5d968c90 100644
--- a/tests/lean/defeq_simp2.lean
+++ b/tests/lean/defeq_simp2.lean
@@ -10,7 +10,7 @@ axiom foo3 (n : nat) : n ≥ 0
 example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchanged := ff} >>= trace,
+  e ← get_local `H >>= infer_type, s^.dsimplify [] e {fail_if_unchanged := ff} >>= trace,
   constructor
 
 constant x1 : nat -- update the environment to force defeq_canonize cache to be reset
@@ -18,7 +18,7 @@ constant x1 : nat -- update the environment to force defeq_canonize cache to be
 example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchanged := ff} >>= trace,
+  e ← get_local `H >>= infer_type, s^.dsimplify [] e {fail_if_unchanged := ff} >>= trace,
   constructor
 
 constant x2 : nat -- update the environment to force defeq_canonize cache to be reset
diff --git a/tests/lean/defeq_simp4.lean b/tests/lean/defeq_simp4.lean
index 20508e1d8e..41703ad2b9 100644
--- a/tests/lean/defeq_simp4.lean
+++ b/tests/lean/defeq_simp4.lean
@@ -16,10 +16,10 @@ set_option pp.all true
 example (a b : nat) (H : (λ x : nat, @has_add.add nat (nat_has_add3 x) a b) = (λ x : nat, @has_add.add nat nat_has_add2 a x)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchanged := ff} >>= trace,
+  e ← get_local `H >>= infer_type, s^.dsimplify [] e {fail_if_unchanged := ff} >>= trace,
   trace "---------",
   -- The following should work
   e ← get_local `H >>= infer_type,
-  e ← s^.dsimplify e {fail_if_unchanged := ff},
-  s^.dsimplify e {fail_if_unchanged := ff} >>= trace,
+  e ← s^.dsimplify [] e {fail_if_unchanged := ff},
+  s^.dsimplify [] e {fail_if_unchanged := ff} >>= trace,
   constructor
diff --git a/tests/lean/dsimp_whnf.lean b/tests/lean/dsimp_whnf.lean
index fe395c0aba..d4ea67b6b8 100644
--- a/tests/lean/dsimp_whnf.lean
+++ b/tests/lean/dsimp_whnf.lean
@@ -2,6 +2,6 @@ open tactic
 
 example (a b : nat) : ((a + 1, b).1) = a + 1 :=
 by do
-  dsimp,
+  dsimp_target,
   trace_state,
   reflexivity
diff --git a/tests/lean/run/cases_tac1.lean b/tests/lean/run/cases_tac1.lean
index 5d9b0dcf57..1c5bc1c499 100644
--- a/tests/lean/run/cases_tac1.lean
+++ b/tests/lean/run/cases_tac1.lean
@@ -25,7 +25,7 @@ by do
   w ← get_local `w,
   cases w [`n', `hw, `tw],
   trace_state,
-  dsimp,
+  dsimp_target,
   trace_state,
   Heq1 ← intro1,
   Heq2 ← intro1,
diff --git a/tests/lean/run/dsimp_proj.lean b/tests/lean/run/dsimp_proj.lean
new file mode 100644
index 0000000000..5e97c89ccf
--- /dev/null
+++ b/tests/lean/run/dsimp_proj.lean
@@ -0,0 +1,14 @@
+example (a b : nat) : a + b = b + a :=
+begin
+  dsimp [has_add.add],
+  guard_target nat.add a b = nat.add b a,
+  apply add_comm
+end
+
+example (f g : nat → nat) : (f ∘ g) = (λ x, f (g x)) :=
+begin
+  fail_if_success {dsimp},
+  dsimp {unfold_reducible := tt},
+  guard_target (λ x, f (g x)) = (λ x, f (g x)),
+  refl
+end
diff --git a/tests/lean/run/kabstract_cache.lean b/tests/lean/run/kabstract_cache.lean
index 6f6905b68f..fb2bf6f91b 100644
--- a/tests/lean/run/kabstract_cache.lean
+++ b/tests/lean/run/kabstract_cache.lean
@@ -2,6 +2,6 @@ open tactic
 
 example {α : Type} (f : α → α → α) (a b : α) (H₁ : a = b) (H₂ : f b a = a) :
 let c := a in f c c = c :=
-by do dsimp,
+by do dsimp_target,
       e ← get_local `H₁, rewrite_target e {occs := occurrences.pos [1]},
       get_local `H₂ >>= exact