Fixing bug #3285.

1 files changed, 8 insertions, 1 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8c4cec0c2..cc02f6135 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