From 49c38a4254df8f0ace8d94ba08e3762d44bee298 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 21 Mar 2012 14:41:39 +0000
Subject: 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
---
 proofs/pfedit.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9be475ac42..02401dc03e 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
-- 
cgit v1.2.3