From a3c404ac3bce1109ebd3e5906bfd77eeb90a6643 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 21 Aug 2015 15:45:52 -0700 Subject: [PATCH] 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 | 21 ++++++++++++++------- tests/lean/run/apply_failure.lean | 5 +++++ 2 files changed, 19 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/apply_failure.lean diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index aed4ad1981..ba13cc2c7b 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/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 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 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(); + } }); } diff --git a/tests/lean/run/apply_failure.lean b/tests/lean/run/apply_failure.lean new file mode 100644 index 0000000000..245bcbeb68 --- /dev/null +++ b/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