diff options
| -rw-r--r-- | proofs/pfedit.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2f3f58dc30..0b9ff097f4 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -63,7 +63,8 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook = let goals = [ (Global.env_of_context hyps , c) ] in let init_tac = Option.map Proofview.V82.tactic init_tac in Proof_global.start_proof id str goals ?compute_guard hook; - Option.iter Proof_global.run_tactic init_tac + try Option.iter Proof_global.run_tactic init_tac + with e -> Proof_global.discard_current (); raise e let restart_proof () = undo_todepth 1 |