diff --git a/library/init/meta/async_tactic.lean b/library/init/meta/async_tactic.lean
index 106795551e..2fa6cf663a 100644
--- a/library/init/meta/async_tactic.lean
+++ b/library/init/meta/async_tactic.lean
@@ -9,26 +9,29 @@ import init.meta.interactive
 
 namespace tactic
 
+private meta def report {α} (s : tactic_state) : option (unit → format) → α
+| (some fmt) := undefined_core $ to_string $ fmt () ++ format.line ++ to_fmt s
+| none       := undefined_core "silent failure"
+
+
 private meta def run_or_fail {α} (s : tactic_state) (tac : tactic α) : α :=
 match tac s with
 | (tactic_result.success a s) := a
-| (tactic_result.exception .α fmt _ s') :=
-  undefined_core $ to_string $ fmt () ++ format.line ++ to_fmt s'
+| (tactic_result.exception fmt _ s') := report s' fmt
 end
 
 meta def run_async {α : Type} (tac : tactic α) : tactic (task α) := do
 s ← read, return $ task.delay $ λ _,
   match tac s with
   | (tactic_result.success a s) := a
-  | (tactic_result.exception .α fmt _ s') :=
-    undefined_core $ to_string $ fmt () ++ format.line ++ to_fmt s'
+  | (tactic_result.exception fmt _ s') := report s' fmt
   end
 
 meta def prove_goal_async (tac : tactic unit) : tactic unit := do
 ctx ← local_context, revert_lst ctx,
 tgt ← target, tgt ← instantiate_mvars tgt,
 env ← get_env, tgt ← return $ env^.unfold_untrusted_macros tgt,
-when tgt^.has_meta_var (fail $ "goal contains metavariables"),
+when tgt^.has_meta_var (fail "goal contains metavariables"),
 params ← return tgt^.collect_univ_params,
 lemma_name ← new_aux_decl_name,
 proof ← run_async (do
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index ea0ca13c53..1d51f01609 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -26,9 +26,7 @@ meta def istep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_
 meta def rstep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit :=
 λ ss ts, tactic_result.cases_on (istep line col tac ss ts)
   (λ ⟨a, new_ss⟩ new_ts, tactic_result.success ((), new_ss) new_ts)
-  (λ msg_thunk e ts,
-    let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ ts^.to_format in
-        (tactic.report_error line col msg >> tactic.failed) ts)
+  (λ msg_thunk e, tactic.report_exception line col msg_thunk)
 
 meta def execute (tac : smt_tactic unit) : tactic unit :=
 using_smt tac
diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean
index 18813cb0a9..39e1b8c638 100644
--- a/library/init/meta/smt/smt_tactic.lean
+++ b/library/init/meta/smt/smt_tactic.lean
@@ -76,7 +76,7 @@ meta def smt_tactic_orelse {α : Type} (t₁ t₂ : smt_tactic α) : smt_tactic
   tactic_result.success
   (λ e₁ ref₁ s', tactic_result.cases_on (t₂ ss ts)
      tactic_result.success
-     (tactic_result.exception (α × smt_state)))
+     tactic_result.exception)
 
 meta instance : monad_fail smt_tactic :=
 { smt_tactic.monad with fail := λ α s, (tactic.fail (to_fmt s) : smt_tactic α) }
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 5260e19c4d..b901b0ebc6 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -27,8 +27,8 @@ meta instance : has_to_format tactic_state :=
 ⟨tactic_state.to_format⟩
 
 meta inductive tactic_result (α : Type u)
-| success   : α → tactic_state → tactic_result
-| exception : (unit → format) → option expr → tactic_state → tactic_result
+| success      : α → tactic_state → tactic_result
+| exception {} : option (unit → format) → option expr → tactic_state → tactic_result
 
 open tactic_result
 
@@ -37,8 +37,9 @@ variables {α : Type u}
 variables [has_to_string α]
 
 meta def tactic_result_to_string : tactic_result α → string
-| (success a s)          := to_string a
-| (exception .α t ref s) := "Exception: " ++ to_string (t ())
+| (success a s)              := to_string a
+| (exception (some t) ref s) := "Exception: " ++ to_string (t ())
+| (exception none ref s)     := "[silent exception]"
 
 meta instance : has_to_string (tactic_result α) :=
 ⟨tactic_result_to_string⟩
@@ -54,12 +55,12 @@ variables {α : Type u} {β : Type v}
 @[inline] meta def tactic_fmap (f : α → β) (t : tactic α) : tactic β :=
 λ s, tactic_result.cases_on (t s)
   (λ a s', success (f a) s')
-  (λ e s', exception β e s')
+  (λ e s', exception e s')
 
 @[inline] meta def tactic_bind (t₁ : tactic α) (t₂ : α → tactic β) : tactic β :=
 λ s,  tactic_result.cases_on (t₁ s)
   (λ a s', t₂ a s')
-  (λ e s', exception β e s')
+  (λ e s', exception e s')
 
 @[inline] meta def tactic_return (a : α) : tactic α :=
 λ s, success a s
@@ -69,7 +70,7 @@ meta def tactic_orelse {α : Type u} (t₁ t₂ : tactic α) : tactic α :=
   success
   (λ e₁ ref₁ s', tactic_result.cases_on (t₂ s)
      success
-     (exception α))
+     exception)
 
 @[inline] meta def tactic_seq (t₁ : tactic α) (t₂ : tactic β) : tactic β :=
 tactic_bind t₁ (λ a, t₂)
@@ -81,8 +82,14 @@ end
 meta instance : monad tactic :=
 {map := @tactic_fmap, ret := @tactic_return, bind := @tactic_bind}
 
+meta def tactic.mk_exception {α : Type u} {β : Type v} [has_to_format β] (msg : β) (ref : option expr) (s : tactic_state) : tactic_result α :=
+exception (some (λ _, to_fmt msg)) none s
+
 meta def tactic.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : tactic α :=
-λ s, exception α (λ u, to_fmt msg) none s
+λ s, tactic.mk_exception msg none s
+
+meta def tactic.silent_fail {α : Type u} : tactic α :=
+λ s, exception none none s
 
 meta def tactic.failed {α : Type u} : tactic α :=
 tactic.fail "failed"
@@ -95,14 +102,14 @@ meta instance : alternative tactic :=
 
 meta def {u₁ u₂} tactic.up {α : Type u₂} (t : tactic α) : tactic (ulift.{u₁} α) :=
 λ s, match t s with
-| success a s'         := success (ulift.up a) s'
-| exception .α t ref s := exception (ulift α) t ref s
+| success a s'      := success (ulift.up a) s'
+| exception t ref s := exception t ref s
 end
 
 meta def {u₁ u₂} tactic.down {α : Type u₂} (t : tactic (ulift.{u₁} α)) : tactic α :=
 λ s, match t s with
 | success (ulift.up a) s' := success a s'
-| exception .(ulift α) t ref s := exception α t ref s
+| exception t ref s       := exception t ref s
 end
 
 namespace tactic
@@ -121,7 +128,7 @@ try_core t >> skip
 
 meta def fail_if_success {α : Type u} (t : tactic α) : tactic unit :=
 λ s, tactic_result.cases_on (t s)
- (λ a s, exception _ (λ _, to_fmt "fail_if_success combinator failed, given tactic succeeded") none s)
+ (λ a s, mk_exception "fail_if_success combinator failed, given tactic succeeded" none s)
  (λ e ref s', success () s)
 
 open list
@@ -145,21 +152,25 @@ repeat_at_most 100000
 
 meta def returnex {α : Type} (e : exceptional α) : tactic α :=
 λ s, match e with
-| (exceptional.success a)       := tactic_result.success a s
-| (exceptional.exception .α f) := tactic_result.exception α (λ u, f options.mk) none s -- TODO(Leo): extract options from environment
+| exceptional.success a      := success a s
+| exceptional.exception .α f := exception (some (λ u, f options.mk)) none s -- TODO(Leo): extract options from environment
 end
 
 meta def returnopt (e : option α) : tactic α :=
 λ s, match e with
-| (some a) := tactic_result.success a s
-| none     := tactic_result.exception α (λ u, to_fmt "failed") none s
+| (some a) := success a s
+| none     := mk_exception "failed" none s
 end
 
 /- Decorate t's exceptions with msg -/
 meta def decorate_ex (msg : format) (t : tactic α) : tactic α :=
 λ s, tactic_result.cases_on (t s)
   success
-  (λ e, exception α (λ u, msg ++ format.nest 2 (format.line ++ e u)))
+  (λ opt_thunk,
+     match opt_thunk with
+     | some e := exception (some (λ u, msg ++ format.nest 2 (format.line ++ e u)))
+     | none   := exception none
+     end)
 
 @[inline] meta def write (s' : tactic_state) : tactic unit :=
 λ s, success () s'
@@ -461,14 +472,18 @@ t >>[tactic] cleanup
 meta def istep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic unit :=
 λ s, @scope_trace _ line col ((t >>[tactic] cleanup) s)
 
+meta def report_exception {α : Type} (line col : nat) : option (unit → format) → tactic α
+| (some msg_thunk) := λ s,
+  let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ s^.to_format in
+  (tactic.report_error line col msg >> silent_fail) s
+| none := silent_fail
+
 /- Auxiliary definition used to implement begin ... end blocks.
    It is similar to step, but it reports an error at the given line/col if the tactic t fails. -/
 meta def rstep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic unit :=
 λ s, tactic_result.cases_on (istep line col t s)
   (λ a new_s, tactic_result.success () new_s)
-  (λ msg_thunk e new_s,
-    let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
-        (tactic.report_error line col msg >> tactic.failed) new_s)
+  (λ msg_thunk e, report_exception line col msg_thunk)
 
 meta def is_prop (e : expr) : tactic bool :=
 do t ← infer_type e,
diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 4d42e42217..8be03a7729 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -48,7 +48,7 @@ expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & par
     auto c_pos  = p.pos();
     name c_name;
     if (is_example) {
-        c_name = get_this_tk();
+        c_name = "_example";
     } else {
         if (!is_instance)
             parse_univ_params(p, lp_names);
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 81b999c016..96b4659b31 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2858,18 +2858,21 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
     tactic_state s       = mk_tactic_state_for(mvar);
 
     try {
-        tactic_state new_s = tactic_evaluator(m_ctx, m_opts)(s, tactic, ref);
-
-        metavar_context mctx = new_s.mctx();
-        expr val = mctx.instantiate_mvars(new_s.main());
-        if (has_expr_metavar(val)) {
-            val = recoverable_error(some_expr(type), ref,
-                                    unsolved_tactic_state(new_s, "tactic failed, result contains meta-variables", ref));
+        if (optional<tactic_state> new_s = tactic_evaluator(m_ctx, m_opts)(s, tactic, ref)) {
+            metavar_context mctx = new_s->mctx();
+            expr val = mctx.instantiate_mvars(new_s->main());
+            if (has_expr_metavar(val)) {
+                val = recoverable_error(some_expr(type), ref,
+                                        unsolved_tactic_state(*new_s, "tactic failed, result contains meta-variables", ref));
+            }
+            mctx.assign(mvar, val);
+            m_env = new_s->env();
+            m_ctx.set_env(m_env);
+            m_ctx.set_mctx(mctx);
+        } else {
+            m_ctx.assign(mvar, mk_sorry(some_expr(type), ref));
+            m_has_errors = true;
         }
-        mctx.assign(mvar, val);
-        m_env = new_s.env();
-        m_ctx.set_env(m_env);
-        m_ctx.set_mctx(mctx);
     } catch (std::exception & ex) {
         if (try_report(ex, some_expr(ref))) {
             m_ctx.assign(mvar, mk_sorry(some_expr(type), ref));
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index c979ebb5f6..3a1d7c059b 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/module_mgr.h"
 #include "library/export_decl.h"
 #include "library/trace.h"
+#include "library/quote.h"
 #include "library/class.h"
 #include "library/exception.h"
 #include "library/aliases.h"
@@ -341,16 +342,24 @@ expr parser::rec_save_pos(expr const & e, pos_info p) {
 expr parser::copy_with_new_pos(expr const & e, pos_info p) {
     switch (e.kind()) {
     case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta:
-    case expr_kind::Local: case expr_kind::Var:
+    case expr_kind::Var:  case expr_kind::Local:
         return save_pos(copy(e), p);
     case expr_kind::App:
         return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
                                        copy_with_new_pos(app_arg(e), p)),
                         p);
-    case expr_kind::Lambda: case expr_kind::Pi:
-        return save_pos(update_binding(e,
-                                       copy_with_new_pos(binding_domain(e), p),
-                                       copy_with_new_pos(binding_body(e), p)),
+    case expr_kind::Lambda:
+        return save_pos(::lean::mk_lambda(binding_name(e),
+                                          copy_with_new_pos(binding_domain(e), p),
+                                          copy_with_new_pos(binding_body(e), p),
+                                          binding_info(e)),
+
+                        p);
+    case expr_kind::Pi:
+        return save_pos(::lean::mk_pi(binding_name(e),
+                                      copy_with_new_pos(binding_domain(e), p),
+                                      copy_with_new_pos(binding_body(e), p),
+                                      binding_info(e)),
                         p);
     case expr_kind::Let:
         return save_pos(::lean::mk_let(let_name(e),
@@ -358,12 +367,16 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
                                        copy_with_new_pos(let_value(e), p),
                                        copy_with_new_pos(let_body(e), p)),
                         p);
-    case expr_kind::Macro: {
-        buffer<expr> args;
-        for (unsigned i = 0; i < macro_num_args(e); i++)
-            args.push_back(copy_with_new_pos(macro_arg(e, i), p));
-        return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
-    }}
+    case expr_kind::Macro:
+        if (is_quote(e)) {
+            return save_pos(mk_quote_core(copy_with_new_pos(get_quote_expr(e), p)), p);
+        } else {
+            buffer<expr> args;
+            for (unsigned i = 0; i < macro_num_args(e); i++)
+                args.push_back(copy_with_new_pos(macro_arg(e, i), p));
+            return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
+        }
+    }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index d90bc37cfe..41edf4b387 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -498,6 +498,8 @@ public:
         in_notation_ctx(parser & p):m_ctx(p.m_scanner) {}
     };
 
+    bool in_notation() const { return m_scanner.in_notation(); }
+
 public:
     /* pos_info_provider API */
     virtual optional<pos_info> get_pos_info(expr const & e) const override;
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index fa0ff46017..cb351a8b75 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -103,6 +103,8 @@ public:
     public:
         in_notation_ctx(scanner & s):m_in_notation(s.m_in_notation, true) {}
     };
+
+    bool in_notation() const { return m_in_notation; }
 };
 std::ostream & operator<<(std::ostream & out, token_kind k);
 bool is_id_rest(char const * begin, char const * end);
diff --git a/src/frontends/lean/tactic_evaluator.cpp b/src/frontends/lean/tactic_evaluator.cpp
index ef9ddc07c1..5bd567628f 100644
--- a/src/frontends/lean/tactic_evaluator.cpp
+++ b/src/frontends/lean/tactic_evaluator.cpp
@@ -82,29 +82,31 @@ static void process_failure(vm_state & S, vm_obj const & r, expr const & ref) {
         else
             throw_unsolved_tactic_state(s1, fmt, ref);
     }
+    /* Do nothing if it is a silent failure */
+    lean_assert(is_tactic_silent_exception(r));
 }
 
-tactic_state tactic_evaluator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref) {
+optional<tactic_state> tactic_evaluator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref) {
     name tactic_name("_tactic");
     environment new_env = compile_tactic(tactic_name, tactic);
     vm_state S(new_env, m_opts);
     vm_obj r = invoke_tactic(S, tactic_name, {to_obj(s)});
 
     if (optional<tactic_state> new_s = is_tactic_success(r)) {
-        return *new_s;
+        return new_s;
     }
     process_failure(S, r, ref);
-    lean_unreachable();
+    return optional<tactic_state>();
 }
 
-tactic_state tactic_evaluator::execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref) {
-    tactic_state new_s = execute_tactic(tactic, s, ref);
-    if (new_s.goals())
-        throw_unsolved_tactic_state(new_s, "tactic failed, there are unsolved goals", ref);
+optional<tactic_state> tactic_evaluator::execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref) {
+    optional<tactic_state> new_s = execute_tactic(tactic, s, ref);
+    if (new_s && new_s->goals())
+        throw_unsolved_tactic_state(*new_s, "tactic failed, there are unsolved goals", ref);
     return new_s;
 }
 
-tactic_state tactic_evaluator::operator()(tactic_state const & s, expr const & tactic, expr const & ref) {
+optional<tactic_state> tactic_evaluator::operator()(tactic_state const & s, expr const & tactic, expr const & ref) {
     return execute_atomic(s, tactic, ref);
 }
 
diff --git a/src/frontends/lean/tactic_evaluator.h b/src/frontends/lean/tactic_evaluator.h
index 8bfb2e3878..36efd9689c 100644
--- a/src/frontends/lean/tactic_evaluator.h
+++ b/src/frontends/lean/tactic_evaluator.h
@@ -21,11 +21,11 @@ class tactic_evaluator {
     environment compile_tactic(name const & tactic_name, expr const & tactic);
     vm_obj invoke_tactic(vm_state & S, name const & tactic_name, std::initializer_list<vm_obj> const & args);
 
-    tactic_state execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref);
-    tactic_state execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref);
+    optional<tactic_state> execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref);
+    optional<tactic_state> execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref);
 public:
     tactic_evaluator(type_context & ctx, options const & opts);
 
-    tactic_state operator()(tactic_state const & s, expr const & tactic, expr const & ref);
+    optional<tactic_state> operator()(tactic_state const & s, expr const & tactic, expr const & ref);
 };
 }
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 36d567c899..bdbe905c5b 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -60,6 +60,8 @@ static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name cons
 }
 
 static expr mk_tactic_rstep(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool report_error) {
+    if (p.in_notation())
+        return mk_tactic_step(p, tac, pos, tac_class);
     if (tac.get_tag() == nulltag)
         tac = p.save_pos(tac, pos);
     name c;
@@ -570,8 +572,8 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     p.clear_expr_locals();
     auto tac_pos = p.pos();
     try {
-        bool use_rstep    = false;
-        bool report_error = false;
+        bool use_rstep    = true;
+        bool report_error = true;
         expr tac  = parse_tactic(p, get_tactic_name(), use_rstep, report_error);
         expr type = mk_tactic_unit(get_tactic_name());
         expr r    = p.save_pos(mk_typed_expr(type, tac), tac_pos);
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 97e59a9bec..d2852ebecb 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -466,10 +466,29 @@ struct add_decl_sorry_check : public task<unit> {
     bool is_tiny() const override { return true; }
     task_kind get_kind() const override { return task_kind::elab; }
 
+    optional<name> should_report_sorry(name const & n) {
+        if (n.is_anonymous())
+            return optional<name>();
+        if (!is_internal_name(n))
+            return optional<name>(n);
+        if (!n.is_string() || n.is_atomic())
+            return optional<name>();
+        if (strcmp(n.get_string(), "_main") == 0)
+            return should_report_sorry(n.get_prefix());
+        if (strncmp(n.get_string(), "_match", 6) == 0) {
+            // TODO(Leo): we may report the same function multiple times,
+            // if it contains many nested match-expressions containing sorry.
+            return should_report_sorry(n.get_prefix());
+        }
+        return optional<name>();
+    }
+
     unit execute() override {
         if (has_sorry(m_decl)) {
-            report_message(message(get_module_id(), m_pos, WARNING,
-                                   (sstream() << "declaration '" << m_decl.get_name() << "' uses sorry").str()));
+            if (optional<name> n = should_report_sorry(m_decl.get_name())) {
+                report_message(message(get_module_id(), m_pos, WARNING,
+                                       (sstream() << "declaration '" << *n << "' uses sorry").str()));
+            }
         }
         return {};
     }
diff --git a/src/library/quote.h b/src/library/quote.h
index bf31da0c48..5f7e80ddf4 100644
--- a/src/library/quote.h
+++ b/src/library/quote.h
@@ -11,6 +11,7 @@ namespace lean {
 expr mk_quote(expr const & e);
 bool is_quote(expr const & e);
 expr const & get_quote_expr(expr const & e);
+expr mk_quote_core(expr const & e);
 
 expr mk_antiquote(expr const & e);
 bool is_antiquote(expr const & e);
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index 369e590638..6d15be0f65 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -273,8 +273,8 @@ optional<tactic_state> is_tactic_success(vm_obj const & o) {
 }
 
 optional<tactic_exception_info> is_tactic_exception(vm_state & S, vm_obj const & ex) {
-    if (is_constructor(ex) && cidx(ex) == 1) {
-        vm_obj fmt = S.invoke(cfield(ex, 0), mk_vm_unit());
+    if (is_constructor(ex) && cidx(ex) == 1 && !is_none(cfield(ex, 0))) {
+        vm_obj fmt = S.invoke(get_some_value(cfield(ex, 0)), mk_vm_unit());
         optional<expr> ref;
         if (!is_none(cfield(ex, 1)))
             ref = to_expr(get_some_value(cfield(ex, 1)));
@@ -284,6 +284,10 @@ optional<tactic_exception_info> is_tactic_exception(vm_state & S, vm_obj const &
     }
 }
 
+bool is_tactic_silent_exception(vm_obj const & ex) {
+    return is_constructor(ex) && cidx(ex) == 1 && is_none(cfield(ex, 0));
+}
+
 vm_obj mk_tactic_result(vm_obj const & a, vm_obj const & s) {
     lean_assert(is_tactic_state(s));
     return mk_vm_constructor(0, a, s);
@@ -316,11 +320,11 @@ vm_obj mk_tactic_success(tactic_state const & s) {
 }
 
 vm_obj mk_tactic_exception(vm_obj const & fn, tactic_state const & s) {
-    return mk_vm_constructor(1, fn, mk_vm_none(), to_obj(s));
+    return mk_vm_constructor(1, mk_vm_some(fn), mk_vm_none(), to_obj(s));
 }
 
 vm_obj mk_tactic_exception(vm_obj const & fn, vm_obj const & ref, tactic_state const & s) {
-    return mk_vm_constructor(1, fn, ref, to_obj(s));
+    return mk_vm_constructor(1, mk_vm_some(fn), ref, to_obj(s));
 }
 
 vm_obj mk_tactic_exception(throwable const & ex, tactic_state const & s) {
diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h
index a6d96b5aae..5e12ed988a 100644
--- a/src/library/tactic/tactic_state.h
+++ b/src/library/tactic/tactic_state.h
@@ -155,6 +155,7 @@ typedef std::tuple<format, optional<expr>, tactic_state> tactic_exception_info;
 /* If ex is (base_tactic_result.exception fn), then return (fn ()).
    The vm_state S is used to execute (fn ()). */
 optional<tactic_exception_info> is_tactic_exception(vm_state & S, vm_obj const & ex);
+bool is_tactic_silent_exception(vm_obj const & ex);
 
 type_context mk_type_context_for(tactic_state const & s, transparency_mode m = transparency_mode::Semireducible);
 type_context mk_type_context_for(tactic_state const & s, local_context const & lctx, transparency_mode m = transparency_mode::Semireducible);
diff --git a/tests/lean/1162.lean.expected.out b/tests/lean/1162.lean.expected.out
index 9db580af70..e6dd4e316e 100644
--- a/tests/lean/1162.lean.expected.out
+++ b/tests/lean/1162.lean.expected.out
@@ -1,3 +1,2 @@
 1162.lean:10:12: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
 1162.lean:7:4: warning: declaration 'ppday' uses sorry
-1162.lean:7:4: warning: declaration 'ppday.equations._eqn_1' uses sorry
diff --git a/tests/lean/1258.lean.expected.out b/tests/lean/1258.lean.expected.out
index fedb555b53..65a2f864c2 100644
--- a/tests/lean/1258.lean.expected.out
+++ b/tests/lean/1258.lean.expected.out
@@ -6,10 +6,3 @@ foo : ∀ (ns : list ℕ), P xs ns,
 n : ℕ,
 ns : list ℕ
 ⊢ P xs (n :: ns)
-1258.lean:4:54: error: failed
-state:
-xs : list ℕ,
-foo : ∀ (ns : list ℕ), P xs ns,
-n : ℕ,
-ns : list ℕ
-⊢ P xs (n :: ns)
diff --git a/tests/lean/1277.lean.expected.out b/tests/lean/1277.lean.expected.out
index 7607fa9beb..f3a2730945 100644
--- a/tests/lean/1277.lean.expected.out
+++ b/tests/lean/1277.lean.expected.out
@@ -8,11 +8,3 @@ f₁ : α₁ → α₁,
 f₂ : Π ⦃a : α₁⦄, α₂ a → α₂ (f₁ a),
 eq₁ : f₁ = id
 ⊢ map f₁ f₂ = id
-1277.lean:9:0: error: failed
-state:
-α₁ : Type,
-α₂ : α₁ → Type,
-f₁ : α₁ → α₁,
-f₂ : Π ⦃a : α₁⦄, α₂ a → α₂ (f₁ a),
-eq₁ : f₁ = id
-⊢ map f₁ f₂ = id
diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out
index 888bdd949f..946d899075 100644
--- a/tests/lean/anc1.lean.expected.out
+++ b/tests/lean/anc1.lean.expected.out
@@ -1,6 +1,5 @@
 (1, 2) : ℕ × ℕ
 and.intro trivial trivial : true ∧ true
-anc1.lean:5:8: warning: declaration '_example' uses sorry
 {fst := 1, snd := sorry} : Σ' (x : ℕ), x > 0
 show true, from true.intro : true
 Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
diff --git a/tests/lean/auto_quote_error.lean.expected.out b/tests/lean/auto_quote_error.lean.expected.out
index 198dc35514..626e54dace 100644
--- a/tests/lean/auto_quote_error.lean.expected.out
+++ b/tests/lean/auto_quote_error.lean.expected.out
@@ -10,9 +10,3 @@ a b c : ℕ,
 h1 : a = b,
 h2 : b = c
 ⊢ c = a
-auto_quote_error.lean:6:0: error: failed
-state:
-a b c : ℕ,
-h1 : a = b,
-h2 : b = c
-⊢ c = a
diff --git a/tests/lean/auto_quote_error2.lean.expected.out b/tests/lean/auto_quote_error2.lean.expected.out
index 7a77d8b107..182c99de54 100644
--- a/tests/lean/auto_quote_error2.lean.expected.out
+++ b/tests/lean/auto_quote_error2.lean.expected.out
@@ -8,17 +8,6 @@ a_1 : a = b,
 a_2 : b = c
 ⊢ a = c
 
-a b c : ℕ,
-a_1 : a = b,
-a_2 : b = c
-⊢ Sort ?
-auto_quote_error2.lean:8:0: error: failed
-state:
-a b c : ℕ,
-a_1 : a = b,
-a_2 : b = c
-⊢ a = c
-
 a b c : ℕ,
 a_1 : a = b,
 a_2 : b = c
@@ -30,12 +19,6 @@ a b c : ℕ,
 a_1 : a = b,
 a_2 : b = c
 ⊢ a = c
-auto_quote_error2.lean:19:0: error: failed
-state:
-a b c : ℕ,
-a_1 : a = b,
-a_2 : b = c
-⊢ a = c
 hello world
 auto_quote_error2.lean:28:2: error: focus tactic failed, focused goal has not been solved
 state:
@@ -43,12 +26,6 @@ a b c : ℕ,
 a_1 : a = b,
 a_2 : b = c
 ⊢ a = ?m_1
-auto_quote_error2.lean:30:0: error: failed
-state:
-a b c : ℕ,
-a_1 : a = b,
-a_2 : b = c
-⊢ a = ?m_1
 auto_quote_error2.lean:37:22: error: don't know how to synthesize placeholder
 context:
 a b c : ℕ,
@@ -61,15 +38,3 @@ a b c : ℕ,
 h1 : a = b,
 h2 : b = c
 ⊢ a = c
-auto_quote_error2.lean:38:2: error: failed
-state:
-a b c : ℕ,
-h1 : a = b,
-h2 : b = c
-⊢ a = c
-auto_quote_error2.lean:39:0: error: failed
-state:
-a b c : ℕ,
-h1 : a = b,
-h2 : b = c
-⊢ a = c
diff --git a/tests/lean/aux_decl_zeta.lean.expected.out b/tests/lean/aux_decl_zeta.lean.expected.out
index e6c2910386..94b1284b3e 100644
--- a/tests/lean/aux_decl_zeta.lean.expected.out
+++ b/tests/lean/aux_decl_zeta.lean.expected.out
@@ -8,6 +8,4 @@ has type
   vec ℕ n
 but is expected to have type
   vec ℕ 10
-aux_decl_zeta.lean:5:11: warning: declaration 'f._main' uses sorry
-aux_decl_zeta.lean:5:11: warning: declaration 'f._main.equations._eqn_1' uses sorry
-aux_decl_zeta.lean:5:11: warning: declaration 'f.equations._eqn_1' uses sorry
+aux_decl_zeta.lean:5:11: warning: declaration 'f' uses sorry
diff --git a/tests/lean/bad_error2.lean.expected.out b/tests/lean/bad_error2.lean.expected.out
index e33610e40c..838f3039fa 100644
--- a/tests/lean/bad_error2.lean.expected.out
+++ b/tests/lean/bad_error2.lean.expected.out
@@ -7,13 +7,3 @@ _match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
 w : ℕ,
 hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
 ⊢ n + w = m
-bad_error2.lean:10:4: error: failed
-state:
-k n m : ℕ,
-h : k + n ≤ k + m,
-_match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
-w : ℕ,
-hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
-⊢ n + w = m
-bad_error2.lean:3:8: warning: declaration 'this._match_1' uses sorry
-bad_error2.lean:3:8: warning: declaration 'this._match_1.equations._eqn_1' uses sorry
diff --git a/tests/lean/bad_error3.lean.expected.out b/tests/lean/bad_error3.lean.expected.out
index 31c518e6fd..3ea1971fe2 100644
--- a/tests/lean/bad_error3.lean.expected.out
+++ b/tests/lean/bad_error3.lean.expected.out
@@ -11,4 +11,3 @@ state:
 p : ℕ → ℕ → Prop
 ⊢ sorry
 bad_error3.lean:5:4: warning: declaration 'ex' uses sorry
-bad_error3.lean:5:4: warning: declaration 'ex.equations._eqn_1' uses sorry
diff --git a/tests/lean/bad_error4.lean.expected.out b/tests/lean/bad_error4.lean.expected.out
index 75b4e31612..76cb379781 100644
--- a/tests/lean/bad_error4.lean.expected.out
+++ b/tests/lean/bad_error4.lean.expected.out
@@ -7,4 +7,3 @@ has type
 but is expected to have type
   unit → unit
 bad_error4.lean:4:11: warning: declaration 'bar' uses sorry
-bad_error4.lean:4:11: warning: declaration 'bar.equations._eqn_1' uses sorry
diff --git a/tests/lean/bad_error5.lean.expected.out b/tests/lean/bad_error5.lean.expected.out
index da606e4a82..275ed4cd97 100644
--- a/tests/lean/bad_error5.lean.expected.out
+++ b/tests/lean/bad_error5.lean.expected.out
@@ -1,3 +1,8 @@
-bad_error5.lean:13:10: error: _tactic._val_3: trying to evaluate sorry
+bad_error5.lean:13:10: error: don't know how to synthesize placeholder
+context:
+c : S
+⊢ Type ?
+bad_error5.lean:13:10: error: failed to add declaration '_tactic' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  …
 bad_error5.lean:9:11: warning: declaration 'V' uses sorry
-bad_error5.lean:9:11: warning: declaration 'V.equations._eqn_1' uses sorry
diff --git a/tests/lean/bad_inaccessible.lean.expected.out b/tests/lean/bad_inaccessible.lean.expected.out
index 5e88fcab16..238b2a1cb2 100644
--- a/tests/lean/bad_inaccessible.lean.expected.out
+++ b/tests/lean/bad_inaccessible.lean.expected.out
@@ -1,13 +1,10 @@
 bad_inaccessible.lean:3:5: error: invalid use of inaccessible term, it is not fixed by other arguments
 bad_inaccessible.lean:2:11: warning: declaration 'f1' uses sorry
-bad_inaccessible.lean:2:11: warning: declaration 'f1.equations._eqn_1' uses sorry
 bad_inaccessible.lean:6:7: error: invalid use of inaccessible term, the provided term is
   b
 but is expected to be
   a
 bad_inaccessible.lean:5:11: warning: declaration 'f2' uses sorry
-bad_inaccessible.lean:5:11: warning: declaration 'f2.equations._eqn_1' uses sorry
 bad_inaccessible.lean:14:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
 bad_inaccessible.lean:12:11: warning: declaration 'foo' uses sorry
-bad_inaccessible.lean:12:11: warning: declaration 'foo.equations._eqn_1' uses sorry
diff --git a/tests/lean/bad_inaccessible2.lean.expected.out b/tests/lean/bad_inaccessible2.lean.expected.out
index 80d20ffec1..237af993a3 100644
--- a/tests/lean/bad_inaccessible2.lean.expected.out
+++ b/tests/lean/bad_inaccessible2.lean.expected.out
@@ -8,4 +8,3 @@ but is expected to have type
   vec A .(.?m_2 + 1)
 bad_inaccessible2.lean:31:46: error: ill-formed match/equations expression
 bad_inaccessible2.lean:29:11: warning: declaration 'map_head' uses sorry
-bad_inaccessible2.lean:29:11: warning: declaration 'map_head.equations._eqn_1' uses sorry
diff --git a/tests/lean/cls_err.lean.expected.out b/tests/lean/cls_err.lean.expected.out
index a02918c0b4..1e51638450 100644
--- a/tests/lean/cls_err.lean.expected.out
+++ b/tests/lean/cls_err.lean.expected.out
@@ -2,4 +2,3 @@ cls_err.lean:13:2: error: failed to synthesize type class instance for
 A : Type u
 ⊢ H A
 cls_err.lean:12:13: warning: declaration 'tst' uses sorry
-cls_err.lean:12:13: warning: declaration 'tst.equations._eqn_1' uses sorry
diff --git a/tests/lean/crash.lean.expected.out b/tests/lean/crash.lean.expected.out
index b415d97e26..6faee8713c 100644
--- a/tests/lean/crash.lean.expected.out
+++ b/tests/lean/crash.lean.expected.out
@@ -17,4 +17,3 @@ H : P,
 H' : ¬P
 ⊢ sorry
 crash.lean:6:11: warning: declaration 'crash' uses sorry
-crash.lean:6:11: warning: declaration 'crash.equations._eqn_1' uses sorry
diff --git a/tests/lean/ctx.lean.expected.out b/tests/lean/ctx.lean.expected.out
index c545974691..c02c5723db 100644
--- a/tests/lean/ctx.lean.expected.out
+++ b/tests/lean/ctx.lean.expected.out
@@ -7,4 +7,3 @@ h : A = B,
 p1 p2 : A × B
 ⊢ ℕ
 ctx.lean:2:11: warning: declaration 'foo' uses sorry
-ctx.lean:2:11: warning: declaration 'foo.equations._eqn_1' uses sorry
diff --git a/tests/lean/do_match_fail.lean.expected.out b/tests/lean/do_match_fail.lean.expected.out
index 10e3957cbc..5f273e18d5 100644
--- a/tests/lean/do_match_fail.lean.expected.out
+++ b/tests/lean/do_match_fail.lean.expected.out
@@ -4,10 +4,4 @@ p q : Prop,
 a : p,
 a_1 : q
 ⊢ p
-do_match_fail.lean:9:0: error: failed
-state:
-p q : Prop,
-a : p,
-a_1 : q
-⊢ p
 do_match_fail.lean:20:3: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
index 2c0e7cadab..89ce929abc 100644
--- a/tests/lean/elab_error_msgs.lean.expected.out
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -9,7 +9,6 @@ but is expected to have type
 Additional information:
 elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
 elab_error_msgs.lean:5:4: warning: declaration 'bogus_elim' uses sorry
-elab_error_msgs.lean:5:4: warning: declaration 'bogus_elim.equations._eqn_1' uses sorry
 elab_error_msgs.lean:9:0: error: type mismatch at application
   bogus_elim trivial
 term
diff --git a/tests/lean/elab_error_recovery.lean.expected.out b/tests/lean/elab_error_recovery.lean.expected.out
index b74383f107..8dc434a78e 100644
--- a/tests/lean/elab_error_recovery.lean.expected.out
+++ b/tests/lean/elab_error_recovery.lean.expected.out
@@ -12,7 +12,13 @@ half_baked : ℕ → ℕ
 elab_error_recovery.lean:8:8: error: failed to synthesize type class instance for
 half_baked : ℕ → ℕ
 ⊢ decidable (2 ∈ 3)
-elab_error_recovery.lean:10:11: error: undefined
+elab_error_recovery.lean:10:11: error: don't know how to synthesize placeholder
+context:
+half_baked : ℕ → ℕ
+⊢ Type ?
+elab_error_recovery.lean:10:11: error: failed to add declaration '_tactic' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  …
 elab_error_recovery.lean:12:14: error: invalid type ascription, expression has type
   list ?m_1
 but is expected to have type
@@ -21,11 +27,6 @@ state:
 half_baked : ℕ → ℕ,
 _x : ℕ
 ⊢ ℕ
-elab_error_recovery.lean:12:23: error: failed
-state:
-half_baked : ℕ → ℕ,
-_x : ℕ
-⊢ ℕ
 elab_error_recovery.lean:6:8: error: don't know how to synthesize placeholder
 context:
 half_baked : ℕ → ℕ
@@ -34,18 +35,7 @@ elab_error_recovery.lean:8:29: error: don't know how to synthesize placeholder
 context:
 half_baked : ℕ → ℕ
 ⊢ ℕ
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_1' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_2' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_3' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_4' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_5' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_6' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_2' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_3' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_4' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_5' uses sorry
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked.equations._eqn_6' uses sorry
+elab_error_recovery.lean:1:4: warning: declaration 'half_baked' uses sorry
 def half_baked._main : ℕ → ℕ :=
 λ (a : ℕ),
   ite (a = 3) 2
diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out
index a06e596d6c..a596cf86ed 100644
--- a/tests/lean/empty.lean.expected.out
+++ b/tests/lean/empty.lean.expected.out
@@ -1,4 +1,3 @@
 empty.lean:6:39: error: failed to synthesize type class instance for
 ⊢ nonempty Empty
 empty.lean:6:25: warning: declaration 'v2' uses sorry
-empty.lean:6:25: warning: declaration 'v2.equations._eqn_1' uses sorry
diff --git a/tests/lean/eqn_hole.lean.expected.out b/tests/lean/eqn_hole.lean.expected.out
index a126c26bfe..e7ad3e3c43 100644
--- a/tests/lean/eqn_hole.lean.expected.out
+++ b/tests/lean/eqn_hole.lean.expected.out
@@ -4,7 +4,6 @@ f : ℕ → ℕ
 ⊢ ℕ
 eqn_hole.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 eqn_hole.lean:2:11: warning: declaration 'f' uses sorry
-eqn_hole.lean:2:11: warning: declaration 'f.equations._eqn_1' uses sorry
 eqn_hole.lean:8:13: error: don't know how to synthesize placeholder
 context:
 g : ℕ → ℕ,
@@ -12,4 +11,3 @@ n : ℕ
 ⊢ ℕ
 eqn_hole.lean:6:11: error: support for well-founded recursion has not been implemented yet, use 'set_option trace.eqn_compiler true' for additional information
 eqn_hole.lean:6:11: warning: declaration 'g' uses sorry
-eqn_hole.lean:6:11: warning: declaration 'g.equations._eqn_1' uses sorry
diff --git a/tests/lean/error_pos.lean.expected.out b/tests/lean/error_pos.lean.expected.out
index 65614b9b53..cc60ff69aa 100644
--- a/tests/lean/error_pos.lean.expected.out
+++ b/tests/lean/error_pos.lean.expected.out
@@ -1,6 +1,5 @@
 error_pos.lean:1:39: error: type expected at
   B
-error_pos.lean:1:8: warning: declaration '_example' uses sorry
 error_pos.lean:4:43: error: type expected at
   B
 error_pos.lean:9:39: error: type expected at
diff --git a/tests/lean/hole_in_fn.lean.expected.out b/tests/lean/hole_in_fn.lean.expected.out
index 4e91b14057..eacabdaae1 100644
--- a/tests/lean/hole_in_fn.lean.expected.out
+++ b/tests/lean/hole_in_fn.lean.expected.out
@@ -3,4 +3,3 @@ context:
 n : ℕ
 ⊢ ℕ
 hole_in_fn.lean:5:11: warning: declaration 'f' uses sorry
-hole_in_fn.lean:5:11: warning: declaration 'f.equations._eqn_1' uses sorry
diff --git a/tests/lean/hole_issue2.lean.expected.out b/tests/lean/hole_issue2.lean.expected.out
index 09e7acc9d5..96167fffa5 100644
--- a/tests/lean/hole_issue2.lean.expected.out
+++ b/tests/lean/hole_issue2.lean.expected.out
@@ -1,5 +1,4 @@
 hole_issue2.lean:12:25: warning: declaration 'count' uses sorry
-hole_issue2.lean:12:25: warning: declaration 'count.equations._eqn_1' uses sorry
 hole_issue2.lean:22:74: error: don't know how to synthesize placeholder
 context:
 A : Type,
@@ -11,8 +10,7 @@ h : ⟦l₁⟧ ⊆ ⟦l₂⟧,
 w : A,
 hw : ¬list.count w l₁ ≤ list.count w l₂
 ⊢ false
-hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1._match_1' uses sorry
-hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1._match_1.equations._eqn_1' uses sorry
+hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1' uses sorry
 hole_issue2.lean:29:65: error: don't know how to synthesize placeholder
 context:
 A : Type,
@@ -22,8 +20,7 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false
-hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2._match_1' uses sorry
-hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2._match_1.equations._eqn_1' uses sorry
+hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2' uses sorry
 hole_issue2.lean:36:28: error: don't know how to synthesize placeholder
 context:
 A : Type,
@@ -33,5 +30,4 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ false
-hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3._match_1' uses sorry
-hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3._match_1.equations._eqn_1' uses sorry
+hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3' uses sorry
diff --git a/tests/lean/inaccessible.lean.expected.out b/tests/lean/inaccessible.lean.expected.out
index a6756e168c..1a11f459b4 100644
--- a/tests/lean/inaccessible.lean.expected.out
+++ b/tests/lean/inaccessible.lean.expected.out
@@ -4,7 +4,6 @@ inaccessible.lean:14:2: error: invalid occurrence of macro expression in pattern
   sorry
 inaccessible.lean:14:17: error: ill-formed match/equations expression
 inaccessible.lean:13:11: warning: declaration 'inv_3' uses sorry
-inaccessible.lean:13:11: warning: declaration 'inv_3.equations._eqn_1' uses sorry
 inaccessible.lean:17:11: error: invalid inaccessible annotation, it cannot be used around functions in applications
 inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
 inaccessible.lean:28:3: error: function expected at
@@ -19,9 +18,7 @@ but is expected to have type
   imf f sorry
 inaccessible.lean:28:16: error: ill-formed match/equations expression
 inaccessible.lean:27:11: warning: declaration 'inv_7' uses sorry
-inaccessible.lean:27:11: warning: declaration 'inv_7.equations._eqn_1' uses sorry
 inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
 inaccessible.lean:82:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
 inaccessible.lean:80:11: warning: declaration 'map_6' uses sorry
-inaccessible.lean:80:11: warning: declaration 'map_6.equations._eqn_1' uses sorry
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index 0c224db7a0..1f2e69ae58 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -4,10 +4,8 @@ inaccessible2.lean:5:4: error: invalid use of inaccessible term, the provided te
 but is expected to be
   f a
 inaccessible2.lean:4:11: warning: declaration 'inv_1' uses sorry
-inaccessible2.lean:4:11: warning: declaration 'inv_1.equations._eqn_1' uses sorry
 inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
 inaccessible2.lean:11:11: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
 inaccessible2.lean:14:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
 inaccessible2.lean:14:20: error: ill-formed match/equations expression
 inaccessible2.lean:13:11: warning: declaration 'symm' uses sorry
-inaccessible2.lean:13:11: warning: declaration 'symm.equations._eqn_1' uses sorry
diff --git a/tests/lean/instance_cache1.lean.expected.out b/tests/lean/instance_cache1.lean.expected.out
index 4abee50bfd..c6ae8091b8 100644
--- a/tests/lean/instance_cache1.lean.expected.out
+++ b/tests/lean/instance_cache1.lean.expected.out
@@ -4,18 +4,15 @@ a : A,
 this : has_add A
 ⊢ has_add A
 instance_cache1.lean:1:11: warning: declaration 'f1' uses sorry
-instance_cache1.lean:1:11: warning: declaration 'f1.equations._eqn_1' uses sorry
 instance_cache1.lean:6:7: error: failed to synthesize type class instance for
 A : Type ?,
 a : A,
 s : has_add A
 ⊢ has_add A
 instance_cache1.lean:5:11: warning: declaration 'f2' uses sorry
-instance_cache1.lean:5:11: warning: declaration 'f2.equations._eqn_1' uses sorry
 instance_cache1.lean:9:19: error: failed to synthesize type class instance for
 A : Type ?,
 a : A,
 s : has_add A
 ⊢ has_add A
 instance_cache1.lean:8:11: warning: declaration 'f3' uses sorry
-instance_cache1.lean:8:11: warning: declaration 'f3.equations._eqn_1' uses sorry
diff --git a/tests/lean/interactive/do_info.lean.expected.out b/tests/lean/interactive/do_info.lean.expected.out
index e3737d2496..79e7e330d2 100644
--- a/tests/lean/interactive/do_info.lean.expected.out
+++ b/tests/lean/interactive/do_info.lean.expected.out
@@ -1,7 +1,7 @@
-{"msg":{"caption":"trace output","file_name":"f","pos_col":0,"pos_line":3,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
+{"msg":{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":496},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
+{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":511},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
 {"record":{"full-id":"tactic.transitivity","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":30},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":9}
-{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":603},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
+{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":618},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
 {"record":{"full-id":"tactic.symmetry","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":27},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":14}
-{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":603},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}
+{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":618},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}
diff --git a/tests/lean/interactive/my_tac_class.lean b/tests/lean/interactive/my_tac_class.lean
index 99814a66e7..36ab1c99d5 100644
--- a/tests/lean/interactive/my_tac_class.lean
+++ b/tests/lean/interactive/my_tac_class.lean
@@ -18,9 +18,9 @@ t >> return ()
 meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
 λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
   (λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
-  (λ msg_thunk e new_s,
-    let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
-        (tactic.report_error line col msg >> tactic.failed) new_s)
+  (λ opt_msg_thunk e new_s, match opt_msg_thunk with
+    | some msg_thunk := let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
+        (tactic.report_error line col msg >> tactic.silent_fail) new_s | none := tactic.silent_fail new_s end)
 
 meta def execute (tac : mytac unit) : tactic unit :=
 tac 0 >> return ()
diff --git a/tests/lean/interactive/rb_map_ts.lean b/tests/lean/interactive/rb_map_ts.lean
index d18084ed49..19cecc1fe7 100644
--- a/tests/lean/interactive/rb_map_ts.lean
+++ b/tests/lean/interactive/rb_map_ts.lean
@@ -18,9 +18,9 @@ t >> return ()
 meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
 λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
   (λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
-  (λ msg_thunk e new_s,
-    let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
-        (tactic.report_error line col msg >> tactic.failed) new_s)
+  (λ opt_msg_thunk e new_s, match opt_msg_thunk with
+        | some msg_thunk :=  let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
+        (tactic.report_error line col msg >> tactic.silent_fail) new_s | none := tactic.silent_fail new_s end)
 
 meta def execute (tac : mytac unit) : tactic unit :=
 tac (name_map.mk nat) >> return ()
diff --git a/tests/lean/minimize_errors.lean.expected.out b/tests/lean/minimize_errors.lean.expected.out
index e1e2f9da72..2353d324c6 100644
--- a/tests/lean/minimize_errors.lean.expected.out
+++ b/tests/lean/minimize_errors.lean.expected.out
@@ -5,7 +5,6 @@ has type
 but is expected to have type
   ℕ → ℕ → ℕ
 minimize_errors.lean:1:4: warning: declaration 'f' uses sorry
-minimize_errors.lean:1:4: warning: declaration 'f.equations._eqn_1' uses sorry
 f : ℕ → ℕ → ℕ
 g : ℕ → ℕ → ℕ
 def g : ℕ → ℕ → ℕ :=
diff --git a/tests/lean/nested_errors.lean.expected.out b/tests/lean/nested_errors.lean.expected.out
index bc39b0705b..7ee5fa38c1 100644
--- a/tests/lean/nested_errors.lean.expected.out
+++ b/tests/lean/nested_errors.lean.expected.out
@@ -4,15 +4,3 @@ a b c : ℕ,
 a_1 : a = b,
 a_2 : c = b
 ⊢ a = c
-nested_errors.lean:7:2: error: failed
-state:
-a b c : ℕ,
-a_1 : a = b,
-a_2 : c = b
-⊢ a = c
-nested_errors.lean:8:0: error: failed
-state:
-a b c : ℕ,
-a_1 : a = b,
-a_2 : c = b
-⊢ a = c
diff --git a/tests/lean/non_exhaustive_error.lean.expected.out b/tests/lean/non_exhaustive_error.lean.expected.out
index 87bf1e69d8..64298dfb31 100644
--- a/tests/lean/non_exhaustive_error.lean.expected.out
+++ b/tests/lean/non_exhaustive_error.lean.expected.out
@@ -1,3 +1,2 @@
 non_exhaustive_error.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 non_exhaustive_error.lean:2:11: warning: declaration 'f' uses sorry
-non_exhaustive_error.lean:2:11: warning: declaration 'f.equations._eqn_1' uses sorry
diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out
index d49b118ee6..d925317acc 100644
--- a/tests/lean/quot_bug.lean.expected.out
+++ b/tests/lean/quot_bug.lean.expected.out
@@ -1,2 +1 @@
 λ (x : A), f x
-quot_bug.lean:8:8: warning: declaration '_example' uses sorry
diff --git a/tests/lean/run/774.lean b/tests/lean/run/774.lean
index b1c5d7093c..92518303c2 100644
--- a/tests/lean/run/774.lean
+++ b/tests/lean/run/774.lean
@@ -3,4 +3,4 @@ example : ℕ → ℕ → Prop
 | 0 0               := true
 | (succ n) 0        := false
 | 0 (succ m)        := false
-| (succ n) (succ m) := this n m
+| (succ n) (succ m) := _example n m
diff --git a/tests/lean/run/isabelle.lean b/tests/lean/run/isabelle.lean
index 6031a294ab..d17a49eb9c 100644
--- a/tests/lean/run/isabelle.lean
+++ b/tests/lean/run/isabelle.lean
@@ -52,7 +52,7 @@ open lazy_list
 meta def of_tactic {α : Type u} (t : tactic α) : lazy_tactic α :=
 λ s, match t s with
 | tactic_result.success a new_s    := lazy_list.singleton (a, new_s)
-| tactic_result.exception .α f e s := lazy_list.nil
+| tactic_result.exception f e s := lazy_list.nil
 end
 
 meta instance {α : Type} : has_coe (tactic α) (lazy_tactic α) :=
diff --git a/tests/lean/run/my_tac_class.lean b/tests/lean/run/my_tac_class.lean
index 1f23042720..90b1206fe0 100644
--- a/tests/lean/run/my_tac_class.lean
+++ b/tests/lean/run/my_tac_class.lean
@@ -18,9 +18,13 @@ t >> return ()
 meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
 λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
   (λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
-  (λ msg_thunk e new_s,
-    let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
-        (tactic.report_error line col msg >> tactic.failed) new_s)
+  (λ opt_msg_thunk e new_s,
+    match opt_msg_thunk with
+    | some msg_thunk :=
+      let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
+          (tactic.report_error line col msg >> tactic.silent_fail) new_s
+    | none := tactic.silent_fail new_s
+    end)
 
 meta def execute (tac : mytac unit) : tactic unit :=
 tac 0 >> return ()
diff --git a/tests/lean/run/using_smt3.lean b/tests/lean/run/using_smt3.lean
index d2cfae2aba..6c2c836c5f 100644
--- a/tests/lean/run/using_smt3.lean
+++ b/tests/lean/run/using_smt3.lean
@@ -7,8 +7,8 @@ open tactic_result
 
 meta def fail_if_success {α : Type} (t : smt_tactic α) : smt_tactic unit :=
 λ ss ts, match t ss ts with
-| success _ _                         := failed ts
-| exception .(α × smt_state) _ _ _ := success ((), ss) ts
+| success _ _     := failed ts
+| exception _ _ _ := success ((), ss) ts
 end
 
 def my_smt_config : smt_config :=
diff --git a/tests/lean/set_attr1.lean.expected.out b/tests/lean/set_attr1.lean.expected.out
index 4e41ee0617..86e0c2ddd4 100644
--- a/tests/lean/set_attr1.lean.expected.out
+++ b/tests/lean/set_attr1.lean.expected.out
@@ -3,4 +3,3 @@ state:
 n : ℕ
 ⊢ f n = n + 1
 set_attr1.lean:13:11: warning: declaration 'ex2' uses sorry
-set_attr1.lean:13:11: warning: declaration 'ex2.equations._eqn_1' uses sorry
diff --git a/tests/lean/structure_instance_bug.lean.expected.out b/tests/lean/structure_instance_bug.lean.expected.out
index d29092f90c..8508dc43d2 100644
--- a/tests/lean/structure_instance_bug.lean.expected.out
+++ b/tests/lean/structure_instance_bug.lean.expected.out
@@ -1,3 +1,2 @@
 structure_instance_bug.lean:11:0: error: invalid structure value {...}, field 'B' is implicit and must not be provided
 structure_instance_bug.lean:10:11: warning: declaration 'foo3' uses sorry
-structure_instance_bug.lean:10:11: warning: declaration 'foo3.equations._eqn_1' uses sorry
diff --git a/tests/lean/structure_instance_bug2.lean.expected.out b/tests/lean/structure_instance_bug2.lean.expected.out
index 620003a6f3..285d1aafd2 100644
--- a/tests/lean/structure_instance_bug2.lean.expected.out
+++ b/tests/lean/structure_instance_bug2.lean.expected.out
@@ -1,3 +1,2 @@
 structure_instance_bug2.lean:4:0: error: invalid structure instance, 'default_smt_pre_config' is not the name of a structure type
 structure_instance_bug2.lean:3:4: warning: declaration 'my_pre_config1' uses sorry
-structure_instance_bug2.lean:3:4: warning: declaration 'my_pre_config1.equations._eqn_1' uses sorry
diff --git a/tests/lean/tactic_state_pp.lean b/tests/lean/tactic_state_pp.lean
index 2b871b6a4c..8bc0f0b051 100644
--- a/tests/lean/tactic_state_pp.lean
+++ b/tests/lean/tactic_state_pp.lean
@@ -16,8 +16,8 @@ do t     ← target,
 
 meta def pp_state (s : tactic_state) : format :=
 match pp_state_core s with
-| tactic_result.success r _             := r
-| tactic_result.exception .format _ _ _ := "failed to pretty print"
+| tactic_result.success r _     := r
+| tactic_result.exception _ _ _ := "failed to pretty print"
 end
 
 meta instance i2 : has_to_format tactic_state :=
diff --git a/tests/lean/vm_sorry.lean.expected.out b/tests/lean/vm_sorry.lean.expected.out
index 75e604bc27..45dfdfa091 100644
--- a/tests/lean/vm_sorry.lean.expected.out
+++ b/tests/lean/vm_sorry.lean.expected.out
@@ -1,10 +1,5 @@
-vm_sorry.lean:1:4: warning: declaration 'half_baked._main' uses sorry
-vm_sorry.lean:1:4: warning: declaration 'half_baked._main.equations._eqn_1' uses sorry
-vm_sorry.lean:1:4: warning: declaration 'half_baked.equations._eqn_1' uses sorry
+vm_sorry.lean:1:4: warning: declaration 'half_baked' uses sorry
 42
 vm_sorry.lean:6:0: error: half_baked._main._val_1: trying to evaluate sorry
 vm_sorry.lean:12:0: error: undefined
 (some nat)
-vm_sorry.lean:18:8: warning: declaration '_example' uses sorry
-vm_sorry.lean:19:8: warning: declaration '_example' uses sorry
-vm_sorry.lean:20:8: warning: declaration '_example' uses sorry