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/pfedit.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 45e4a84e..7bac87d2 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -68,7 +68,7 @@ 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 reraise -> Proof_global.discard_current (); raise reraise let restart_proof () = undo_todepth 1 @@ -164,9 +164,9 @@ let build_constant_by_tactic id sign typ tac = let _,(const,_,_,_) = cook_proof (fun _ -> ()) in delete_current_proof (); const - with e -> + with reraise -> delete_current_proof (); - raise e + raise reraise let build_by_tactic env typ tac = let id = id_of_string ("temporary_proof"^string_of_int (next())) in -- cgit v1.2.3