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.

1 files changed, 5 insertions, 1 deletions

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