diff --git a/library/init/meta/async_tactic.lean b/library/init/meta/async_tactic.lean
index e0cab2e866..106795551e 100644
--- a/library/init/meta/async_tactic.lean
+++ b/library/init/meta/async_tactic.lean
@@ -47,7 +47,7 @@ namespace interactive
 open interactive.types
 
 /-- Proves the first goal asynchronously as a separate lemma. -/
-meta def async (tac : itactic) : tactic unit :=
+meta def async (tac : irtactic) : tactic unit :=
 prove_goal_async tac
 
 end interactive
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 1d34d65afd..ed762a998d 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -106,6 +106,15 @@ itactic: parse a nested "interactive" tactic. That is, parse
 meta def itactic : Type :=
 tactic unit
 
+/-
+irtactic: parse a nested "interactive" tactic. That is, parse
+  `(` tactic `)`
+It is similar to itactic, but the interactive mode will report errors
+when any of the nested tactics fail. This is good for tactics such as asynch and abstact.
+-/
+meta def irtactic : Type :=
+tactic unit
+
 /--
 This tactic applies to a goal that is either a Pi/forall or starts with a let binder.
 
@@ -341,7 +350,7 @@ tactic.try
 meta def solve1 : itactic → tactic unit :=
 tactic.solve1
 
-meta def abstract (id : opt_ident) (tac : itactic) : tactic unit :=
+meta def abstract (id : opt_ident) (tac : irtactic) : tactic unit :=
 tactic.abstract tac id
 
 /--
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index e63005ddcb..ea0ca13c53 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -20,8 +20,11 @@ repeat close
 meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit :=
 tac >> solve_goals
 
+meta def istep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit :=
+λ ss ts, @scope_trace _ line col ((tac >> solve_goals) ss ts)
+
 meta def rstep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit :=
-λ ss ts, tactic_result.cases_on (@scope_trace _ line col ((tac >> solve_goals) ss ts))
+λ 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
@@ -39,6 +42,9 @@ open interactive.types
 meta def itactic : Type :=
 smt_tactic unit
 
+meta def irtactic : Type :=
+smt_tactic unit
+
 meta def intros : raw_ident_list → smt_tactic unit
 | [] := smt_tactic.intros
 | hs := smt_tactic.intro_lst hs
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 3931372135..11d4b7b1d6 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -452,10 +452,13 @@ get_goals >>= set_goals
 meta def step {α : Type u} (t : tactic α) : tactic unit :=
 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)
+
 /- 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 (@scope_trace _ line col ((t >>[tactic] cleanup) s))
+λ 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
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 9701e57e94..36d567c899 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -32,15 +32,18 @@ Author: Leonardo de Moura
 
    3) There is a definition: Tac.step {α : Type} (t : Tac α) : Tac unit
 
-   4) (Optional) Tac.rstep {α : Type} (line : nat) (col : nat) (tac : Tac α) : Tac unit
-      similar to Tac.step, but reports an error at the given position if tac fails.
-      If this one if not available, then Tac.step is used.
+   4) (Optional) Tac.istep {α : Type} (line : nat) (col : nat) (tac : Tac α) : Tac unit
+      Similar to step but it should scope trace messages at the given line/col,
 
-   5) There is a definition Tac.save_info (line col : nat) : Tac unit
+   5) (Optional) Tac.rstep {α : Type} (line : nat) (col : nat) (tac : Tac α) (r : bool) : Tac unit
+      Extended step. It should scope trace messages at the given line/col,
+      and report error at line/col if r is tt.
 
-   6) There is a definition Tac.execute (tac : Tac unit) : tactic unit
+   6) There is a definition Tac.save_info (line col : nat) : Tac unit
 
-   7) There is a definition Tac.execute_with (cfg : config) (tac : Tac unit) : tactic unit
+   7) There is a definition Tac.execute (tac : Tac unit) : tactic unit
+
+   8) There is a definition Tac.execute_with (cfg : config) (tac : Tac unit) : tactic unit
       where config is an arbitrary type.
 
    TODO(Leo): improve the "recipe" above. It is too ad hoc.
@@ -56,18 +59,25 @@ static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name cons
     return p.save_pos(mk_app(mk_constant(step_name), tac), pos);
 }
 
-static expr mk_tactic_rstep(parser & p, expr tac, pos_info const & pos, name const & tac_class) {
+static expr mk_tactic_rstep(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool report_error) {
     if (tac.get_tag() == nulltag)
         tac = p.save_pos(tac, pos);
-    name rstep_name(tac_class, "rstep");
-    if (!p.env().find(rstep_name))
+    name c;
+    if (report_error) {
+        c = name(tac_class, "rstep");
+        if (!p.env().find(c))
+            c = name(tac_class, "istep");
+    } else {
+        c = name(tac_class, "istep");
+    }
+    if (!p.env().find(c))
         return mk_tactic_step(p, tac, pos, tac_class);
-    return p.save_pos(mk_app(mk_constant(rstep_name), mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second)), tac), pos);
+    return p.save_pos(mk_app(mk_constant(c), mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second)), tac), pos);
 }
 
-static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep) {
+static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep, bool report_error) {
     if (use_rstep)
-        return mk_tactic_rstep(p, tac, pos, tac_class);
+        return mk_tactic_rstep(p, tac, pos, tac_class, report_error);
     else
         return mk_tactic_step(p, tac, pos, tac_class);
 }
@@ -80,7 +90,7 @@ static expr mk_tactic_save_info(parser & p, pos_info const & pos, name const & t
     return p.save_pos(mk_app(mk_constant(save_info_name), mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second))), pos);
 }
 
-static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep) {
+static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep, bool report_error) {
     if (tac.get_tag() == nulltag)
         tac = p.save_pos(tac, pos);
     name solve1_name(tac_class, "solve1");
@@ -89,7 +99,7 @@ static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name co
                            tac_class << ".solve1' has not been defined", pos);
     expr r = p.save_pos(mk_app(mk_constant(solve1_name), tac), pos);
     if (use_rstep)
-        r = mk_tactic_rstep(p, r, pos, tac_class);
+        r = mk_tactic_rstep(p, r, pos, tac_class, report_error);
     return r;
 }
 
@@ -312,25 +322,25 @@ static expr parse_location(parser & p) {
     }
 }
 
-static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep);
+static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error);
 
-static expr parse_nested_auto_quote_tactic(parser & p, name const & tac_class) {
+static expr parse_nested_auto_quote_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
     auto pos = p.pos();
-    bool use_rstep = false;
     if (p.curr_is_token(get_lcurly_tk())) {
-        return parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class, use_rstep);
+        return parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class, use_rstep, report_error);
     } else if (p.curr_is_token(get_begin_tk())) {
-        return parse_begin_end_block(p, pos, get_end_tk(), tac_class, use_rstep);
+        return parse_begin_end_block(p, pos, get_end_tk(), tac_class, use_rstep, report_error);
     } else {
         throw parser_error("invalid nested auto-quote tactic, '{' or 'begin' expected", pos);
     }
 }
 
-static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep) {
+static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep, bool report_error) {
     auto pos = p.pos();
     p.next();
     expr type    = p.env().get(decl_name).get_type();
     name itactic(name(tac_class, "interactive"), "itactic");
+    name irtactic(name(tac_class, "interactive"), "irtactic");
     buffer<expr> args;
     while (is_pi(type)) {
         if (is_explicit(binding_info(type))) {
@@ -373,7 +383,10 @@ static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name con
                 p.check_token_next(get_comma_tk(), "invalid auto-quote tactic, ',' expected");
                 args.push_back(mk_constant(get_unit_star_name()));
             } else if (is_constant(arg_type, itactic)) {
-                args.push_back(parse_nested_auto_quote_tactic(p, tac_class));
+                bool report_error = false;
+                args.push_back(parse_nested_auto_quote_tactic(p, tac_class, use_rstep, report_error));
+            } else if (is_constant(arg_type, irtactic)) {
+                args.push_back(parse_nested_auto_quote_tactic(p, tac_class, use_rstep, report_error));
             } else {
                 args.push_back(p.parse_expr(get_max_prec()));
             }
@@ -381,7 +394,7 @@ static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name con
         type = binding_body(type);
     }
     expr r = p.mk_app(p.save_pos(mk_constant(decl_name), pos), args, pos);
-    return mk_tactic_step(p, r, pos, tac_class, use_rstep);
+    return mk_tactic_step(p, r, pos, tac_class, use_rstep, report_error);
 }
 
 static bool is_curr_exact_shortcut(parser & p) {
@@ -393,7 +406,7 @@ static bool is_curr_exact_shortcut(parser & p) {
         p.curr_is_token(get_suppose_tk());
 }
 
-static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep) {
+static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
     try {
         p.check_break_before();
         if (p.curr_is_identifier())
@@ -407,24 +420,24 @@ static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep
     expr r;
     auto pos = p.pos();
     if (auto dname = is_auto_quote_tactic(p, tac_class)) {
-        r = parse_auto_quote_tactic(p, *dname, tac_class, use_rstep);
+        r = parse_auto_quote_tactic(p, *dname, tac_class, use_rstep, report_error);
     } else if (is_curr_exact_shortcut(p)) {
         expr arg = parse_qexpr(p, 0);
         r = p.mk_app(p.save_pos(mk_constant(tac_class + name({"interactive", "exact"})), pos), arg, pos);
-        if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class);
+        if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class, report_error);
     } else {
         r = p.parse_expr();
-        if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class);
+        if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class, report_error);
     }
     return concat(p, mk_tactic_save_info(p, pos, tac_class), r, pos);
 }
 
-static expr parse_tactic(parser & p, name const & tac_class, bool use_rstep) {
+static expr parse_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
     if (p.in_quote()) {
         parser::quote_scope _(p, false);
-        return parse_tactic_core(p, tac_class, use_rstep);
+        return parse_tactic_core(p, tac_class, use_rstep, report_error);
     } else {
-        return parse_tactic_core(p, tac_class, use_rstep);
+        return parse_tactic_core(p, tac_class, use_rstep, report_error);
     }
 }
 
@@ -459,7 +472,7 @@ static name parse_tactic_class(parser & p, name tac_class) {
     }
 }
 
-static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep) {
+static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error) {
     p.next();
     name new_tac_class = tac_class;
     if (tac_class == get_tactic_name())
@@ -485,16 +498,16 @@ static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name c
                     name const & end_tk = p.curr_is_token(get_begin_tk()) ? get_end_tk() : get_rcurly_tk();
                     expr info_tac = mk_tactic_save_info(p, pos, tac_class);
                     to_concat.push_back(info_tac);
-                    next_tac = parse_begin_end_block(p, pos, end_tk, tac_class, use_rstep);
+                    next_tac = parse_begin_end_block(p, pos, end_tk, tac_class, use_rstep, report_error);
                     auto block_pos = p.pos_of(next_tac);
-                    next_tac = mk_tactic_solve1(p, next_tac, block_pos, tac_class, use_rstep);
+                    next_tac = mk_tactic_solve1(p, next_tac, block_pos, tac_class, use_rstep, report_error);
                 } else if (p.curr_is_token(get_do_tk())) {
                     expr tac = p.parse_expr();
                     expr type = p.save_pos(mk_tactic_unit(tac_class), pos);
                     next_tac = p.save_pos(mk_typed_expr(type, tac), pos);
-                    next_tac = mk_tactic_step(p, next_tac, pos, tac_class, use_rstep);
+                    next_tac = mk_tactic_step(p, next_tac, pos, tac_class, use_rstep, report_error);
                 } else {
-                    next_tac = parse_tactic(p, tac_class, use_rstep);
+                    next_tac = parse_tactic(p, tac_class, use_rstep, report_error);
                 }
                 to_concat.push_back(next_tac);
                 if (!p.curr_is_token(end_token)) {
@@ -534,7 +547,8 @@ expr parse_begin_end_expr_core(parser & p, pos_info const & pos, name const & en
     parser::local_scope _(p);
     p.clear_expr_locals();
     bool use_rstep = true;
-    expr tac = parse_begin_end_block(p, pos, end_token, get_tactic_name(), use_rstep);
+    bool report_error = true;
+    expr tac = parse_begin_end_block(p, pos, end_token, get_tactic_name(), use_rstep, report_error);
     return copy_tag(tac, mk_by(tac));
 }
 
@@ -556,8 +570,9 @@ 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;
-        expr tac  = parse_tactic(p, get_tactic_name(), use_rstep);
+        bool use_rstep    = false;
+        bool report_error = false;
+        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);
         return p.save_pos(mk_by(r), pos);
@@ -569,11 +584,12 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
 
 expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) {
     name const & tac_class = get_tactic_name();
-    bool use_rstep = false;
-    expr r = parse_tactic(p, tac_class, use_rstep);
+    bool use_rstep    = false;
+    bool report_error = false;
+    expr r = parse_tactic(p, tac_class, use_rstep, report_error);
     while (p.curr_is_token(get_comma_tk())) {
         p.next();
-        expr next = parse_tactic(p, tac_class, use_rstep);
+        expr next = parse_tactic(p, tac_class, use_rstep, report_error);
         r = p.mk_app({p.save_pos(mk_constant(get_pre_monad_and_then_name()), pos), r, next}, pos);
     }
     p.check_token_next(get_rbracket_tk(), "invalid auto-quote tactic block, ']' expected");
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 323632725c..6940af1f5c 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -1005,6 +1005,27 @@ bool get_constructor_rec_args(environment const & env, expr const & e, buffer<pa
     return true;
 }
 
+static expr * g_bool = nullptr;
+static expr * g_bool_tt = nullptr;
+static expr * g_bool_ff = nullptr;
+
+void initialize_bool() {
+    g_bool = new expr(mk_constant(get_bool_name()));
+    g_bool_ff = new expr(mk_constant(get_bool_ff_name()));
+    g_bool_tt = new expr(mk_constant(get_bool_tt_name()));
+}
+
+void finalize_bool() {
+    delete g_bool;
+    delete g_bool_ff;
+    delete g_bool_tt;
+}
+
+expr mk_bool() { return *g_bool; }
+expr mk_bool_tt() { return *g_bool_tt; }
+expr mk_bool_ff() { return *g_bool_tt; }
+expr to_bool_expr(bool b) { return b ? mk_bool_tt() : mk_bool_ff(); }
+
 void initialize_library_util() {
     g_true           = new expr(mk_constant(get_true_name()));
     g_true_intro     = new expr(mk_constant(get_true_intro_name()));
@@ -1015,9 +1036,11 @@ void initialize_library_util() {
     initialize_nat();
     initialize_int();
     initialize_char();
+    initialize_bool();
 }
 
 void finalize_library_util() {
+    finalize_bool();
     finalize_int();
     finalize_nat();
     finalize_char();
diff --git a/src/library/util.h b/src/library/util.h
index beb4336c9b..9203a97e9e 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -272,6 +272,11 @@ optional<expr> get_binary_op(expr const & e, expr & arg1, expr & arg2);
 expr mk_nary_app(expr const & op, buffer<expr> const & nary_args);
 expr mk_nary_app(expr const & op, unsigned num_nary_args, expr const * nary_args);
 
+expr mk_bool();
+expr mk_bool_tt();
+expr mk_bool_ff();
+expr to_bool_expr(bool b);
+
 /* Similar to is_head_beta, but ignores annotations around the function. */
 bool is_annotated_head_beta(expr const & t);
 /* Similar to head_beta_reduce, but also reduces annotations around the function. */
diff --git a/tests/lean/interactive/do_info.lean.expected.out b/tests/lean/interactive/do_info.lean.expected.out
index 1bfccfd5b1..deee7cd398 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"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":476},"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":490},"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":583},"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":597},"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":583},"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":597},"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/info_goal.lean.expected.out b/tests/lean/interactive/info_goal.lean.expected.out
index 53f025bb4d..cf11b367a3 100644
--- a/tests/lean/interactive/info_goal.lean.expected.out
+++ b/tests/lean/interactive/info_goal.lean.expected.out
@@ -1,5 +1,5 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","full-id":"tactic.interactive.exact","source":{"column":9,"file":"/library/init/meta/interactive.lean","line":195},"state":"⊢ ℕ → ℕ","type":"interactive.types.qexpr0 → tactic unit"},"response":"ok","seq_num":4}
+{"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","full-id":"tactic.interactive.exact","source":{"column":9,"file":"/library/init/meta/interactive.lean","line":204},"state":"⊢ ℕ → ℕ","type":"interactive.types.qexpr0 → tactic unit"},"response":"ok","seq_num":4}
 {"record":{"state":"no goals"},"response":"ok","seq_num":6}
 {"record":{"state":"no goals"},"response":"ok","seq_num":8}
 {"record":{"state":"⊢ ℕ → ℕ"},"response":"ok","seq_num":11}
diff --git a/tests/lean/interactive/nested_traces.lean b/tests/lean/interactive/nested_traces.lean
new file mode 100644
index 0000000000..4e0c7f241a
--- /dev/null
+++ b/tests/lean/interactive/nested_traces.lean
@@ -0,0 +1,7 @@
+example (a b c : nat) : a = b → c = b → a = c ∧ b = c :=
+begin
+  intros,
+  split,
+  try { transitivity, trace "hello", assumption, symmetry, assumption },
+  abstract { symmetry, trace "test", assumption }
+end
diff --git a/tests/lean/interactive/nested_traces.lean.expected.out b/tests/lean/interactive/nested_traces.lean.expected.out
new file mode 100644
index 0000000000..6aee00eb68
--- /dev/null
+++ b/tests/lean/interactive/nested_traces.lean.expected.out
@@ -0,0 +1,3 @@
+{"msg":{"caption":"trace output","file_name":"f","pos_col":22,"pos_line":5,"severity":"information","text":"hello\n"},"response":"additional_message"}
+{"msg":{"caption":"trace output","file_name":"f","pos_col":23,"pos_line":6,"severity":"information","text":"test\n"},"response":"additional_message"}
+{"message":"file invalidated","response":"ok","seq_num":0}
diff --git a/tests/lean/nested_errors.lean b/tests/lean/nested_errors.lean
new file mode 100644
index 0000000000..6b5046ad65
--- /dev/null
+++ b/tests/lean/nested_errors.lean
@@ -0,0 +1,8 @@
+example (a b c : nat) : a = b → c = b → a = c ∧ b = c :=
+begin
+  intros,
+  split,
+  try {intro},    -- Should not report the error here
+  repeat {intro}, -- Should not report the error here
+  abstract { intro,  } -- Should report the error in intro tactic
+end
diff --git a/tests/lean/nested_errors.lean.expected.out b/tests/lean/nested_errors.lean.expected.out
new file mode 100644
index 0000000000..bc39b0705b
--- /dev/null
+++ b/tests/lean/nested_errors.lean.expected.out
@@ -0,0 +1,18 @@
+nested_errors.lean:7:13: error: intro tactic failed, Pi/let expression expected
+state:
+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