From 7f92ed9a6e1cd7dd5cc8ecab9a9aea1ff57194cd Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 16 Mar 2013 21:52:51 +0000
Subject: another Errors.push in a exception reraise

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

diff --git a/proofs/proof.ml b/proofs/proof.ml
index d3c3fb71a7..c38f80a553 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -321,7 +321,9 @@ let rec rollback pr =
 let transaction pr t =
   init_transaction pr;
   try t (); commit pr
-  with reraise -> rollback pr; raise reraise
+  with reraise ->
+    let reraise = Errors.push reraise in
+    rollback pr; raise reraise
 
 
 (* Focus command (focuses on the [i]th subgoal) *)
-- 
cgit v1.2.3