Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 4 insertions, 10 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3d507f35..6ac0b553 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -35,8 +35,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
@@ -64,15 +66,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 resume_last_proof () = Proof_global.resume_last ()
-let resume_proof (_,id) = Proof_global.resume id
-let suspend_proof ()  =  Proof_global.suspend ()
+let restart_proof () = undo_todepth 1
 
 let cook_proof hook =
   let prf = Proof_global.give_me_the_proof () in