Pfedit: avoid Undoing too much

 It seems that we can currently do a successful Undo (but not two!)
 on a freshly started Lemma. Let's add a depth check on Pfedit.undo
 to avoid that. This way, we cannot Undo to depth < 1 (with 1 being
 the initial depth of a lemma).

 Simplier implementation of Pfedit.restart : it is Pfedit.undo_todepth 1.

 This extra initial step in the Undo Stack has probably something
 to see with the Lemma argument introduction. For instance, before this
 patch we had:

 Lemma test n : n+0=n.
 Restart. (* now the goal is universally quantified ! *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15075 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 6 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9be475ac4..02401dc03 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -36,8 +36,10 @@ let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
 let delete_all_proofs = Proof_global.discard_all
 
-let undo n = 
+let undo n =
   let p = Proof_global.give_me_the_proof () in
+  let d = Proof.V82.depth p in
+  if n >= d then raise Proof.EmptyUndoStack;
   for i = 1 to n do
     Proof.undo p
   done
@@ -65,11 +67,7 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
   Proof_global.start_proof id str goals ?compute_guard hook;
   Option.iter Proof_global.run_tactic init_tac
 
-let restart_proof () =
-  let p = Proof_global.give_me_the_proof () in
-  try while true do
-    Proof.undo p
-  done with Proof.EmptyUndoStack -> ()
+let restart_proof () = undo_todepth 1
 
 let resume_last_proof () = Proof_global.resume_last ()
 let resume_proof (_,id) = Proof_global.resume id