From aba158dbd46fdb831527fc256eb48f5110632294 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Mar 2015 15:19:19 -0700 Subject: [PATCH] feat(library/tactic/inversion_tactic): improve error message for unknown hypothesis --- src/library/tactic/inversion_tactic.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 037a30102..f3f885d3b 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -1037,8 +1037,11 @@ public: optional execute(goal const & g, name const & n, implementation_list const & imps) { auto p = g.find_hyp(n); - if (!p) + if (!p) { + if (m_throw_tactic_exception) + throw tactic_exception(sstream() << "invalid 'cases' tactic, unknown hypothesis '" << n << "'"); return optional(); + } expr const & h = p->first; return execute(g, h, imps); }