diff options
| author | letouzey | 2012-06-01 14:54:07 +0000 |
|---|---|---|
| committer | letouzey | 2012-06-01 14:54:07 +0000 |
| commit | 6fb13cc6b84ca8f887453bdd825853ccda74fb7f (patch) | |
| tree | 233221efde6e1a9e3ac3e6b1d86012e304f99926 | |
| parent | d2e15d9a8b3024a09dc298cf143073b4649dce43 (diff) | |
Cancel the start of a proof if its init_tac fails (fix #2799)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15407 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |