From 0b4de5132a8fcda6dafe836dd249a4fc69b400fc Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 9 Dec 2013 14:36:30 +0100
Subject: Fix printing of Ltac's backtrace.

I used an exception wrapper to report Tactic failures. It had the consequence of making process_vernac_interp_error to look for the backtrace at the wrong place.---
 toplevel/cerrors.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 96ade04103..afe08053f4 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -114,11 +114,15 @@ let rec process_vernac_interp_error exn = match exn with
          if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
       wrap_vernac_error exn (msg ++ str ".")
-  | Proof_errors.TacticFailure e -> process_vernac_interp_error e
   | exc ->
       exc
 
+let rec strip_wrapping_exceptions = function
+  | Proof_errors.TacticFailure e -> strip_wrapping_exceptions e
+  | exc -> exc
+
 let process_vernac_interp_error exc =
+  let exc = strip_wrapping_exceptions exc in
   let e = process_vernac_interp_error exc in
   let ltac_trace = Exninfo.get exc Proof_type.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc e) in
-- 
cgit v1.2.3