diff --git a/doc/changes.md b/doc/changes.md
index 1e9d7f9cbc..8e89d572ab 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -77,6 +77,10 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 
 * Deleted `simph` and `simp_using_hs` tactics. We should use `simp [*]` instead.
 
+* Use `simp [-h]` and `dsimp [-h]` instead of `simp without h` and `dsimp without h`.
+  Moreover, `simp [*, -h]` if `h` is a hypothesis, we are adding all hypotheses but `h`
+  as additional simplification lemmas.
+
 *API name changes*
 
 * `tactic.dsimp` and `tactic.dsimp_core` => `tactic.dsimp_target`
diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean
index 3bfece4f56..a5bea0c2b1 100644
--- a/library/data/hash_map.lean
+++ b/library/data/hash_map.lean
@@ -270,7 +270,7 @@ section
         have array.read bkts' bidx = f L, from
           show ite (bidx = bidx) _ _ = _, by rw if_pos rfl,
         begin
-          simp[array.iterate_aux] without add_comm,
+          simp[array.iterate_aux, -add_comm],
           rw -(show bidx = ⟨bidx.1, h⟩, from fin.eq_of_veq rfl),
           refine ⟨array.iterate_aux bkts (λ_ bkt r, r ++ bkt) bidx.1 (le_of_lt h) [] ++ u, w, _⟩,
           rw -valid.modify_aux1 _ _ (le_refl _),
@@ -312,7 +312,7 @@ section
         have array.read bkts' bidx = f L, from
           show ite (bidx = bidx) _ _ = _, by rw if_pos rfl,
         begin
-          simp[array.iterate_aux] without add_comm,
+          simp[array.iterate_aux, -add_comm],
           rw [-(show bidx = ⟨bidx.1, h⟩, from fin.eq_of_veq rfl),
               -valid.modify_aux1 _ _ (le_refl _),
               this, hfl, hl],
@@ -365,7 +365,7 @@ theorem valid.replace_aux (a : α) (b : β a) : Π (l : list (Σ a, β a)), a 
 | []           Hc := false.elim Hc
 | (⟨a', b'⟩::t) Hc := begin
   simp at Hc,
-  simp [replace_aux] without and.comm,
+  simp [replace_aux, -and.comm],
   exact match (by apply_instance : decidable (a' = a)) with
   | is_true e := match a', b', e with ._, b', rfl := ⟨[], t, b', rfl, rfl, by simp⟩ end
   | is_false ne :=
diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean
index 5116ec571c..f9898da9bf 100644
--- a/library/init/data/list/lemmas.lean
+++ b/library/init/data/list/lemmas.lean
@@ -110,7 +110,7 @@ by induction l; intros; contradiction
 
 lemma length_remove_nth : ∀ (l : list α) (i : ℕ), i < length l → length (remove_nth l i) = length l - 1
 | []      _     h := rfl
-| (x::xs) 0     h := by simp [remove_nth] without add_comm
+| (x::xs) 0     h := by simp [remove_nth, -add_comm]
 | (x::xs) (i+1) h := have i < length xs, from lt_of_succ_lt_succ h,
   by dsimp [remove_nth]; rw [length_remove_nth xs i this, nat.sub_add_cancel (lt_of_le_of_lt (nat.zero_le _) this)]; refl
 
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index b8a11e1206..29241856e6 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -1163,7 +1163,7 @@ by rw [div_eq_sub_div H (nat.le_add_left _ _), nat.add_sub_cancel]
 by rw [add_comm, add_div_right x H]
 
 @[simp] theorem mul_div_right (n : ℕ) {m : ℕ} (H : m > 0) : m * n / m = n :=
-by {induction n; simp [*, mul_succ] without mul_comm}
+by {induction n; simp [*, mul_succ, -mul_comm]}
 
 @[simp] theorem mul_div_left (m : ℕ) {n : ℕ} (H : n > 0) : m * n / n = m :=
 by rw [mul_comm, mul_div_right _ H]
diff --git a/library/init/meta/converter/interactive.lean b/library/init/meta/converter/interactive.lean
index 245aac42f9..2b3a044e82 100644
--- a/library/init/meta/converter/interactive.lean
+++ b/library/init/meta/converter/interactive.lean
@@ -40,8 +40,8 @@ meta def whnf : conv unit :=
 conv.whnf
 
 meta def dsimp (no_dflt : parse only_flag) (es : parse tactic.simp_arg_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,
+               (cfg : tactic.dsimp_config := {}) : conv unit :=
+do (s, u) ← tactic.mk_simp_set no_dflt attr_names es,
    conv.dsimp (some s) u cfg
 
 meta def trace_lhs : conv unit :=
@@ -109,9 +109,9 @@ do (r, lhs, _) ← tactic.target_lhs_rhs,
   update_lhs new_lhs pr
 
 meta def simp (no_dflt : parse only_flag) (hs : parse tactic.simp_arg_list) (attr_names : parse with_ident_list)
-              (ids : parse without_ident_list) (cfg : tactic.simp_config_ext := {})
+              (cfg : tactic.simp_config_ext := {})
               : conv unit :=
-do (s, u) ← tactic.mk_simp_set no_dflt attr_names hs ids,
+do (s, u) ← tactic.mk_simp_set no_dflt attr_names hs,
    (r, lhs, rhs) ← tactic.target_lhs_rhs,
    (new_lhs, pr) ← tactic.simplify s u lhs cfg.to_simp_config r cfg.discharger,
    update_lhs new_lhs pr,
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 1fc19f0689..ce5c196f87 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -661,27 +661,46 @@ open expr interactive.types
 
 meta inductive simp_arg_type : Type
 | all_hyps : simp_arg_type
+| except   : name  → simp_arg_type
 | expr     : pexpr → simp_arg_type
 
+
 meta instance : has_reflect simp_arg_type
-| simp_arg_type.all_hyps := `(_)
-| (simp_arg_type.expr _) := `(_)
+| simp_arg_type.all_hyps   := `(_)
+| (simp_arg_type.except _) := `(_)
+| (simp_arg_type.expr _)   := `(_)
 
 meta def simp_arg : parser simp_arg_type :=
-(tk "*" *> return simp_arg_type.all_hyps) <|> (simp_arg_type.expr <$> texpr)
+(tk "*" *> return simp_arg_type.all_hyps) <|> (tk "-" *> simp_arg_type.except <$> ident) <|> (simp_arg_type.expr <$> texpr)
 
 meta def simp_arg_list : parser (list simp_arg_type) :=
 list_of simp_arg <|> return []
 
-meta def decode_simp_arg_list (hs : list simp_arg_type) : list pexpr × bool :=
-let r : list pexpr × bool := hs.foldl
-  (λ ⟨es, all⟩ h,
-     match h with
-     | simp_arg_type.all_hyps := (es, tt)
-     | simp_arg_type.expr e   := (e::es, all)
-     end)
-  ([], ff) in
-(r.1.reverse, r.2)
+private meta def resolve_exception_ids (all_hyps : bool) : list name → list name → list name → tactic (list name × list name)
+| []        gex hex := return (gex.reverse, hex.reverse)
+| (id::ids) gex hex := do
+  p ← resolve_name id,
+  let e := p.erase_annotations.get_app_fn.erase_annotations,
+  match e with
+  | const n _           := resolve_exception_ids ids (n::gex) hex
+  | local_const n _ _ _ := when (not all_hyps) (fail $ sformat! "invalid local exception {id}, '*' was not used") >>
+                           resolve_exception_ids ids gex (n::hex)
+  | _                   := fail $ sformat! "invalid exception {id}, unknown identifier"
+  end
+
+/- Return (hs, gex, hex, all) -/
+meta def decode_simp_arg_list (hs : list simp_arg_type) : tactic $ list pexpr × list name × list name × bool :=
+do
+  let (hs, ex, all) := hs.foldl
+    (λ r h,
+       match r, h with
+       | (es, ex, all), simp_arg_type.all_hyps  := (es, ex, tt)
+       | (es, ex, all), simp_arg_type.except id := (es, id::ex, all)
+       | (es, ex, all), simp_arg_type.expr e    := (e::es, ex, all)
+       end)
+    ([], [], ff),
+  (gex, hex) ← resolve_exception_ids all ex [] [],
+  return (hs.reverse, gex, hex, all)
 
 private meta def add_simps : simp_lemmas → list name → tactic simp_lemmas
 | s []      := return s
@@ -721,14 +740,18 @@ private meta def simp_lemmas.append_pexprs : simp_lemmas → list name → list
 | s u []      := return (s, u)
 | s u (l::ls) := do (s, u) ← simp_lemmas.add_pexpr s u l, simp_lemmas.append_pexprs s u ls
 
-meta def mk_simp_set (no_dflt : bool) (attr_names : list name) (hs : list simp_arg_type) (ex : list name) : tactic (simp_lemmas × list name) :=
-do let (hs, add_hyps) := decode_simp_arg_list hs,
+meta def mk_simp_set (no_dflt : bool) (attr_names : list name) (hs : list simp_arg_type) : tactic (simp_lemmas × list name) :=
+do (hs, gex, hex, add_hyps) ← decode_simp_arg_list hs,
    s      ← join_user_simp_lemmas no_dflt attr_names,
    (s, u) ← simp_lemmas.append_pexprs s [] hs,
-   s      ← if add_hyps then collect_ctx_simps >>= s.append else return s,
+   s      ← if add_hyps then do
+              ctx ← collect_ctx_simps,
+              let ctx := ctx.filter (λ h, h.local_uniq_name ∉ hex), -- remove local exceptions
+              s.append ctx
+            else return s,
    -- add equational lemmas, if any
-   ex ← ex.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n),
-   return (simp_lemmas.erase s $ ex.join, u)
+   gex ← gex.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n),
+   return (simp_lemmas.erase s $ gex.join, u)
 
 end mk_simp_set
 
@@ -740,9 +763,9 @@ private meta def simp_hyps (cfg : simp_config) (discharger : tactic unit) (s : s
 | (h::hs) := do h ← get_local h, simp_hyp s u h cfg discharger, simp_hyps hs
 
 meta def simp_core (cfg : simp_config) (discharger : tactic unit)
-                   (no_dflt : bool) (hs : list simp_arg_type) (attr_names : list name) (ids : list name)
+                   (no_dflt : bool) (hs : list simp_arg_type) (attr_names : list name)
                    (locat : loc) : tactic unit :=
-do (s, u) ← mk_simp_set no_dflt attr_names hs ids,
+do (s, u) ← mk_simp_set no_dflt attr_names hs,
    match locat : _ → tactic unit with
    | loc.wildcard :=
      do hs ← non_dep_prop_hyps,
@@ -772,9 +795,11 @@ It has many variants.
    The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.
    This is a convenient way to "unfold" `f`.
 
+- `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.
+
 - `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas
 
-- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,
+- `simp [-id_1, ... -id_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,
    but removes the ones named `id_i`s.
 
 - `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.
@@ -784,20 +809,23 @@ It has many variants.
 - `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.
 -/
 meta def simp (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
-              (ids : parse without_ident_list) (locat : parse location)
-              (cfg : simp_config_ext := {}) : tactic unit :=
-simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names ids locat
+              (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit :=
+simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat
+
+/-- Just construct the simp set and trace it -/
+meta def trace_simp_set (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list) : tactic unit :=
+do (s, _) ← mk_simp_set no_dflt attr_names hs,
+   s.pp >>= trace
 
 /-- Simplify the whole context, and use simplified hypotheses to simplify other hypotheses. -/
-meta def simp_all (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
-                  (ids : parse without_ident_list) (cfg : simp_config_ext := {}) : tactic unit :=
-do (s, u) ← mk_simp_set no_dflt attr_names hs ids,
+meta def simp_all (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list) (cfg : simp_config_ext := {}) : tactic unit :=
+do (s, u) ← mk_simp_set no_dflt attr_names hs,
    tactic.simp_all s u cfg.to_simp_config cfg.discharger,
    try tactic.triv, try (tactic.reflexivity reducible)
 
 meta def simp_intros (ids : parse ident_*) (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
-                     (wo_ids : parse without_ident_list) (cfg : simp_intros_config := {}) : tactic unit :=
-do (s, u) ← mk_simp_set no_dflt attr_names hs wo_ids,
+                     (cfg : simp_intros_config := {}) : tactic unit :=
+do (s, u) ← mk_simp_set no_dflt attr_names hs,
    when (¬u.empty) (fail (sformat! "simp_intros tactic does not support {u}")),
    tactic.simp_intros s u ids cfg,
    try triv >> try (reflexivity reducible)
@@ -808,16 +836,13 @@ hs.mfor' (λ h_name, do h ← get_local h_name, dsimp_hyp h s u cfg)
 private meta def to_simp_arg_list (es : list pexpr) : list simp_arg_type :=
 es.map simp_arg_type.expr
 
-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 :=
+meta def dsimp (no_dflt : parse only_flag) (es : parse simp_arg_list) (attr_names : parse with_ident_list)
+               (l : parse location) (cfg : dsimp_config := {}) : tactic unit :=
+do (s, u) ← mk_simp_set no_dflt attr_names es,
 match l with
-| (loc.ns [])    := do (s, u) ← mk_simp_set no_dflt attr_names (to_simp_arg_list es) ids, dsimp_target s u cfg
-| (loc.ns hs)    := do (s, u) ← mk_simp_set no_dflt attr_names (to_simp_arg_list 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 (to_simp_arg_list es) ids,
-                       dsimp_target s u cfg,
-                       intron n
+| (loc.ns [])    := dsimp_target s u cfg
+| (loc.ns hs)    := dsimp_hyps s u hs cfg
+| (loc.wildcard) := do ls ← local_context, n ← revert_lst ls, dsimp_target s u cfg, intron n
 end
 
 /--
@@ -942,7 +967,7 @@ open interactive interactive.types expr
 meta def unfold (cs : parse ident*) (locat : parse location) (cfg : unfold_config := {}) : tactic unit :=
 do es ← ids_to_simp_arg_list "unfold" cs,
    let no_dflt := tt,
-   simp_core cfg.to_simp_config failed no_dflt es [] [] locat
+   simp_core cfg.to_simp_config failed no_dflt es [] locat
 
 meta def unfold1 (cs : parse ident*) (locat : parse location) (cfg : unfold_config := {single_pass := tt}) : tactic unit :=
 unfold cs locat cfg
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index 6ef5f81b79..1e543c643d 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -252,12 +252,12 @@ slift (tactic.interactive.induction p rec_name ids revert)
 open tactic
 
 /-- Simplify the target type of the main goal. -/
-meta def simp (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list)
+meta def simp (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
               (cfg : simp_config_ext := {}) : smt_tactic unit :=
-tactic.interactive.simp no_dflt hs attr_names ids (loc.ns []) cfg
+tactic.interactive.simp no_dflt hs attr_names (loc.ns []) 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) : smt_tactic unit :=
-tactic.interactive.dsimp no_dflt es attr_names ids (loc.ns [])
+meta def dsimp (no_dflt : parse only_flag) (es : parse simp_arg_list) (attr_names : parse with_ident_list) : smt_tactic unit :=
+tactic.interactive.dsimp no_dflt es attr_names (loc.ns [])
 
 meta def rsimp : smt_tactic unit :=
 do ccs ← to_cc_state, _root_.rsimp.rsimplify_goal ccs
diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out
index eb843ed003..e5546a822d 100644
--- a/tests/lean/interactive/info_tactic.lean.expected.out
+++ b/tests/lean/interactive/info_tactic.lean.expected.out
@@ -1,7 +1,7 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":5,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[(* | expr), ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":6}
-{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":0,"tactic_params":["only?","[(* | expr), ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":8}
-{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":1,"tactic_params":["only?","[(* | expr), ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":10}
-{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":2,"tactic_params":["only?","[(* | expr), ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":12}
+{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp [-id_1, ... -id_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[(* | (- id | expr)), ...]?","(with id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":6}
+{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp [-id_1, ... -id_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":0,"tactic_params":["only?","[(* | (- id | expr)), ...]?","(with id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":8}
+{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp [-id_1, ... -id_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":1,"tactic_params":["only?","[(* | (- id | expr)), ...]?","(with id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":10}
+{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp [-id_1, ... -id_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":2,"tactic_params":["only?","[(* | (- id | expr)), ...]?","(with id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":12}
 {"record":{"full-id":"tactic.get_env","source":,"tactic_params":[],"type":"tactic environment"},"response":"ok","seq_num":14}
diff --git a/tests/lean/run/dsimp_test.lean b/tests/lean/run/dsimp_test.lean
index fd8d3c5571..220bd4b9fc 100644
--- a/tests/lean/run/dsimp_test.lean
+++ b/tests/lean/run/dsimp_test.lean
@@ -52,7 +52,7 @@ end
 
 example (a b c : nat) : g (f 1, f 2) = 41 :=
 begin
-  dsimp [f] without gax,
+  dsimp [f, -gax],
   guard_target g (20 + 0, 20 + 1) = 41,
   dsimp [g],
   guard_target 20 + 0 + (20 + 1) = 41,
diff --git a/tests/lean/run/interactive1.lean b/tests/lean/run/interactive1.lean
index 3fa121f57a..e0f42688e5 100644
--- a/tests/lean/run/interactive1.lean
+++ b/tests/lean/run/interactive1.lean
@@ -41,8 +41,8 @@ attribute [simp] boo bla
 example (a b : nat) : a = b → h 0 a = b :=
 begin
   intro h,
-  simp [h] without bla -- should fail if bla is used
+  simp [h, -bla] -- should fail if bla is used
 end
 open tactic
 example (a b : nat) : a = b → h 0 a = b :=
-by simp without bla {contextual := tt}
+by simp [-bla] {contextual := tt}
diff --git a/tests/lean/simp_except.lean b/tests/lean/simp_except.lean
new file mode 100644
index 0000000000..c53f70dbbc
--- /dev/null
+++ b/tests/lean/simp_except.lean
@@ -0,0 +1,34 @@
+constant f : nat → nat
+
+namespace foo
+axiom fax : ∀ x, f x = x
+end foo
+
+attribute [simp] foo.fax
+
+example (a : nat) : f a = a :=
+by simp -- works
+
+example (a : nat) : f a = a :=
+by simp [-fax] -- Error: unknown identifier 'fax'
+
+example (a : nat) : f a = a :=
+by simp [-foo.fax] -- Error: simplify failed to simplify
+
+section
+open foo
+example (a : nat) : f a = a :=
+by simp [-fax] -- Error: simplify failed to simplify
+end
+
+example (a : nat) (h : a = 0) : a = 0 :=
+by simp [-h] -- Error: invalid local exception h, '*' was not used
+
+example (a : nat) (h : a = 0) : a = 0 :=
+by simp [*, -h] -- Error: simplify failed to simplify
+
+example (a : nat) (h : a = 0) : a = 0 :=
+by simp [*] -- works
+
+example (a b : nat) (h : b = 0) (h₁ : a = b) (h₂ : b = a) : b = 0 :=
+by simp [*, -h₁, -h₂] -- we can prevent loops by removing "bad" hypotheses
diff --git a/tests/lean/simp_except.lean.expected.out b/tests/lean/simp_except.lean.expected.out
new file mode 100644
index 0000000000..6b8b502ecf
--- /dev/null
+++ b/tests/lean/simp_except.lean.expected.out
@@ -0,0 +1,22 @@
+simp_except.lean:13:3: error: unknown identifier 'fax'
+state:
+a : ℕ
+⊢ f a = a
+simp_except.lean:16:3: error: simplify tactic failed to simplify
+state:
+a : ℕ
+⊢ f a = a
+simp_except.lean:21:3: error: simplify tactic failed to simplify
+state:
+a : ℕ
+⊢ f a = a
+simp_except.lean:25:3: error: invalid local exception h, '*' was not used
+state:
+a : ℕ,
+h : a = 0
+⊢ a = 0
+simp_except.lean:28:3: error: simplify tactic failed to simplify
+state:
+a : ℕ,
+h : a = 0
+⊢ a = 0