From ee13513b99cd80bc58a3469b881bd3ee62e3f4c6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Apr 2014 21:56:30 +0200
Subject: Fixing bug #3285.

---
 tactics/tacinterp.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8c4cec0c22..cc02f6135e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2165,7 +2165,14 @@ let _ =
       let tac = out_gen (glbwit wit_tactic) arg in
       let tac = interp_tactic ist tac in
       let prf = Proof.start sigma [env, ty] in
-      let (prf, _) = Proof.run_tactic env tac prf in
+      let (prf, _) =
+        try Proof.run_tactic env tac prf
+        with Proof_errors.TacticFailure e as src ->
+          (** Catch the inner error of the monad tactic *)
+          let src = Errors.push src in
+          let e = Backtrace.app_backtrace ~src ~dst:e in
+          raise e
+      in
       let sigma = Proof.in_proof prf (fun sigma -> sigma) in
       let ans = match Proof.initial_goals prf with
       | [c, _] -> c
-- 
cgit v1.2.3