From 1059ecce2a2662e4d8f335bd4db743df70b100b1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Jan 2014 15:30:01 +0100
Subject: Fixing backtrace handling here and there.

---
 proofs/proofview.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'proofs/proofview.ml')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a0c64d29d0..013b2f2047 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -582,7 +582,9 @@ let tclTIMEOUT n t =
       end
       begin function
         | Proof_errors.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout)
-        | Proof_errors.TacticFailure e -> Proofview_monad.NonLogical.ret (Util.Inr e)
+        | Proof_errors.TacticFailure e as src ->
+          let e = Backtrace.app_backtrace ~src ~dst:e in
+          Proofview_monad.NonLogical.ret (Util.Inr e)
         | e -> Proofview_monad.NonLogical.raise e
       end
   end >>= function
-- 
cgit v1.2.3