From 6fb13cc6b84ca8f887453bdd825853ccda74fb7f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 1 Jun 2012 14:54:07 +0000
Subject: 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
---
 proofs/pfedit.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3