feat(library/tactic/apply_tactic): do not report elaboration failure in apply tactic when proof_state.report_failure() is false

src/library/tactic/apply_tactic.cpp

@@ -207,13 +207,20 @@ tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kin
             goal const & g      = head(gs);
             name_generator ngen = s.get_ngen();
             expr       new_e; substitution new_subst; constraints cs_;
-            auto ecs = elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false);
-            std::tie(new_e, new_subst, cs_) = ecs;
-            buffer<constraint> cs;
-            to_buffer(cs_, cs);
-            to_buffer(s.get_postponed(), cs);
-            proof_state new_s(s, new_subst, ngen, constraints());
-            return apply_tactic_core(env, ios, new_s, new_e, cs, add_meta, k);
+            try {
+                auto ecs = elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false);
+                std::tie(new_e, new_subst, cs_) = ecs;
+                buffer<constraint> cs;
+                to_buffer(cs_, cs);
+                to_buffer(s.get_postponed(), cs);
+                proof_state new_s(s, new_subst, ngen, constraints());
+                return apply_tactic_core(env, ios, new_s, new_e, cs, add_meta, k);
+            } catch (exception &) {
+                if (s.report_failure())
+                    throw;
+                else
+                    return proof_state_seq();
+            }
         });
 }
 

tests/lean/run/apply_failure.lean

@@ -0,0 +1,5 @@
+example (a b c : Prop) : a ∧ b → b ∧ a :=
+begin
+  intro H,
+  repeat (apply or.elim H | apply and.elim H | intro H | split | assumption)
+end