diff options
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r-- | proofs/pfedit.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |