From 120bffce2520f45943cbccbf92602d1cbb9f9c93 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 4 Sep 2016 17:33:26 -0700
Subject: [PATCH] chore(library/equations_compiler/elim_match): add
 cases/induction tactic error message to trace

---
 src/library/equations_compiler/elim_match.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index f19004c3e4..5a28a316a0 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -620,8 +620,8 @@ struct elim_match_fn {
             lean_assert(length(new_goals) == length(new_goal_cnames));
             lean_assert(length(new_goals) == length(ilist));
             lean_assert(length(new_goals) == length(slist));
-        } catch (exception &) {
-            trace_match(tout() << "dependent pattern matching step failed\n";);
+        } catch (exception & ex) {
+            trace_match(tout() << "dependent pattern matching step failed\n" << ex.what() << "\n";);
             throw_error("equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' "
                         "for additional details)");
         }