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