diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index 12851193a..e624f3646 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/src/library/tactic/proof_state.cpp
@@ -31,8 +31,9 @@ bool get_proof_state_goal_names(options const & opts) {
 }
 
 proof_state::proof_state(goals const & gs, substitution const & s, name_generator const & ngen,
-                         constraints const & postponed, bool relax_main_opaque):
-    m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed), m_relax_main_opaque(relax_main_opaque) {
+                         constraints const & postponed, bool relax_main_opaque, bool report_failure):
+    m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed), m_relax_main_opaque(relax_main_opaque),
+    m_report_failure(report_failure) {
     if (std::any_of(gs.begin(), gs.end(),
                     [&](goal const & g) { return s.is_assigned(g.get_mvar()); })) {
         m_goals = filter(gs, [&](goal const & g) { return !s.is_assigned(g.get_mvar()); });
diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h
index b033531b6..e201024c7 100644
--- a/src/library/tactic/proof_state.h
+++ b/src/library/tactic/proof_state.h
@@ -22,17 +22,18 @@ class proof_state {
     name_generator   m_ngen;
     constraints      m_postponed;
     bool             m_relax_main_opaque;
+    bool             m_report_failure;
 
     format pp_core(std::function<formatter()> const & mk_fmt, options const & opts) const;
 
 public:
     proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed,
-                bool relax_main_opaque);
+                bool relax_main_opaque, bool report_failure = true);
     proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen,
                 constraints const & postponed):
-        proof_state(gs, subst, ngen, postponed, s.relax_main_opaque()) {}
+        proof_state(gs, subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {}
     proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen):
-        proof_state(gs, subst, ngen, s.m_postponed, s.m_relax_main_opaque) {}
+        proof_state(gs, subst, ngen, s.m_postponed, s.relax_main_opaque(), s.report_failure()) {}
     proof_state(proof_state const & s, goals const & gs, substitution const & subst):
         proof_state(s, gs, subst, s.m_ngen) {}
     proof_state(proof_state const & s, goals const & gs, name_generator const & ngen):
@@ -40,15 +41,20 @@ public:
     proof_state(proof_state const & s, goals const & gs):
         proof_state(s, gs, s.m_subst) {}
     proof_state(proof_state const & s, name_generator const & ngen, constraints const & postponed):
-        proof_state(s.m_goals, s.m_subst, ngen, postponed, s.m_relax_main_opaque) {}
+        proof_state(s.m_goals, s.m_subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {}
     proof_state(proof_state const & s, name_generator const & ngen):
         proof_state(s, ngen, s.m_postponed) {}
 
+    proof_state update_report_failure(bool f) const {
+        return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, m_relax_main_opaque, f);
+    }
+
     goals const & get_goals() const { return m_goals; }
     substitution const & get_subst() const { return m_subst; }
     name_generator const & get_ngen() const { return m_ngen; }
     constraints const & get_postponed() const { return m_postponed; }
     bool relax_main_opaque() const { return m_relax_main_opaque; }
+    bool report_failure() const { return m_report_failure; }
 
     /** \brief Return true iff this state does not have any goals left */
     bool is_final_state() const { return empty(m_goals); }
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index b920a416b..1fbf4b4c7 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -97,7 +97,8 @@ tactic then(tactic const & t1, tactic const & t2) {
 }
 
 tactic orelse(tactic const & t1, tactic const & t2) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
+            proof_state s = _s.update_report_failure(false);
             return orelse(t1(env, ios, s), t2(env, ios, s), "ORELSE tactical");
         });
 }
@@ -137,31 +138,36 @@ tactic rotate_right(unsigned n) {
 }
 
 tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
+            proof_state s = _s.update_report_failure(false);
             return timeout(t(env, ios, s), ms, check_ms);
         });
 }
 
 tactic append(tactic const & t1, tactic const & t2) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
+            proof_state s = _s.update_report_failure(false);
             return append(t1(env, ios, s), t2(env, ios, s), "APPEND tactical");
         });
 }
 
 tactic interleave(tactic const & t1, tactic const & t2) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
+            proof_state s = _s.update_report_failure(false);
             return interleave(t1(env, ios, s), t2(env, ios, s), "INTERLEAVE tactical");
         });
 }
 
 tactic par(tactic const & t1, tactic const & t2, unsigned check_ms) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
+            proof_state s = _s.update_report_failure(false);
             return par(t1(env, ios, s), t2(env, ios, s), check_ms);
         });
 }
 
 tactic repeat(tactic const & t) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s1) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s1) -> proof_state_seq {
+            proof_state s1 = _s1.update_report_failure(false);
             return repeat(s1, [=](proof_state const & s2) {
                     return t(env, ios, s2);
                 }, "REPEAT tactical");
@@ -169,7 +175,8 @@ tactic repeat(tactic const & t) {
 }
 
 tactic repeat_at_most(tactic const & t, unsigned k) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s1) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s1) -> proof_state_seq {
+            proof_state s1 = _s1.update_report_failure(false);
             return repeat_at_most(s1, [=](proof_state const & s2) {
                     return t(env, ios, s2);
                 }, k, "REPEAT_AT_MOST tactical");
@@ -177,13 +184,15 @@ tactic repeat_at_most(tactic const & t, unsigned k) {
 }
 
 tactic take(tactic const & t, unsigned k) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
+            proof_state s = _s.update_report_failure(false);
             return take(k, t(env, ios, s));
         });
 }
 
 tactic discard(tactic const & t, unsigned k) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
+            proof_state s = _s.update_report_failure(false);
             auto r = t(env, ios, s);
             for (unsigned i = 0; i < k; i++) {
                 auto m = r.pull();