From b35edb34769fecd4dbdf7030222ba3078eab1c93 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Apr 2014 13:59:39 +0200
Subject: Fixing various backtrace recordings.

---
 proofs/pfedit.ml    | 1 +
 proofs/proofview.ml | 5 +++--
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 68c2ed3288..f45eb2a3aa 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -126,6 +126,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
     delete_current_proof ();
     const, status
   with reraise ->
+    let reraise = Errors.push reraise in
     delete_current_proof ();
     raise reraise
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 055cd14b60..22d908e94c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -723,8 +723,9 @@ module V82 = struct
       let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
       let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
-    with Proof_errors.TacticFailure e ->
-      let e = Errors.push e in
+    with Proof_errors.TacticFailure e as src ->
+      let src = Errors.push src in
+      let e = Backtrace.app_backtrace ~src ~dst:e in
       raise e
 
   let put_status b =
-- 
cgit v1.2.3