From 0892990d7bbeb770de458a3b4ef2ffe34a1b11e3 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 28 Jan 2013 21:06:02 +0000
Subject: Actually adding backtrace handling.

I hope I did not forget some [with] clauses. Otherwise, some
stack frame will be missing from the debug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/pfedit.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ef92e8e427..961ff41fb7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -55,7 +55,10 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
    | None -> Proofview.tclUNIT ()
   in
   try Proof_global.run_tactic tac
-  with e -> Proof_global.discard_current (); raise e
+  with e ->
+    let e = Errors.push e in
+    Proof_global.discard_current ();
+    raise e
 
 let restart_proof () = undo_todepth 1
 
-- 
cgit v1.2.3