From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- proofs/proof.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'proofs/proof.ml') diff --git a/proofs/proof.ml b/proofs/proof.ml index a4e556c5..012a4dc1 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -323,7 +323,7 @@ let rec rollback pr = let transaction pr t = init_transaction pr; try t (); commit pr - with e -> rollback pr; raise e + with reraise -> rollback pr; raise reraise (* Focus command (focuses on the [i]th subgoal) *) @@ -429,9 +429,9 @@ let run_tactic env tac pr = let tacticced_proofview = Proofview.apply env tac sp in pr.state <- { pr.state with proofview = tacticced_proofview }; push_undo starting_point pr - with e -> + with reraise -> restore_state starting_point pr; - raise e + raise reraise (*** Commands ***) @@ -476,7 +476,7 @@ module V82 = struct let new_proofview = Proofview.V82.instantiate_evar n com sp in pr.state <- { pr.state with proofview = new_proofview }; push_undo starting_point pr - with e -> + with reraise -> restore_state starting_point pr; - raise e + raise reraise end -- cgit v1.2.3