Fix backtracking bugs:

 - When the undo stack overflows, backtrack within a proof goes to
   wrong state
 - Boundary checks before undoing (popping the stack) wrong


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

1 files changed, 6 insertions, 5 deletions

diff --git a/lib/edit.ml b/lib/edit.ml
index 06a55d171d..e6f2907ecc 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -80,7 +80,7 @@ let undo e n =
     | None -> invalid_arg "Edit.undo"
     | Some d ->
 	let (bs,_) = Hashtbl.find e.buf d in
-	if Bstack.depth bs = 1 & n > 0 then
+	if n >= Bstack.size bs then
 	  errorlabstrm "Edit.undo" (str"Undo stack exhausted");
         repeat n Bstack.pop bs
 
@@ -102,15 +102,16 @@ let undo_todepth e n =
 	else () (* if there is no proof in progress, then n must be zero *)
     | Some d ->
 	let (bs,_) = Hashtbl.find e.buf d in
-	if Bstack.depth bs < n then
+	let ucnt = Bstack.depth bs - n in
+	if  ucnt >= Bstack.size bs then
 	  errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
-        repeat (Bstack.depth bs - n) Bstack.pop bs
+        repeat ucnt Bstack.pop bs
 
-let create e (d,b,c,udepth) =
+let create e (d,b,c,usize) =
   if Hashtbl.mem e.buf d then
     errorlabstrm "Edit.create" 
       (str"Already editing something of that name");
-  let bs = Bstack.create udepth b in
+  let bs = Bstack.create usize b in
   Hashtbl.add e.buf d (bs,c)
 
 let delete e d =