- Documentation de admit et Print Assumptions.

- Relecture, mise à jour, correction d'erreurs et petite
  réorganisation du chapitre sur les commandes vernaculaires.
- Correction bug #1865 (rafraichissement des univers algébriques).
- Suppression de la dépendance du initial.coq en les noms longs des fichiers
  de façons à ce que les dépendances ne soient que purement logique.
- Encore un (petit) bug undo ide.	


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

1 files changed, 7 insertions, 7 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 73fc878b4..afef3b41a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -557,7 +557,7 @@ type backtrack =
 | NoBacktrack
 
 let add_undo (n,a,b) = (n+1,a,b)
-let add_abort (n,a,b) = (n,a+1,b)
+let add_abort (n,a,b) = (0,a+1,b)
 let add_backtrack (n,a,b) b' = (n,a,b')
 
 let pop_command undos t =
@@ -598,16 +598,16 @@ let rec apply_backtrack = function
         end
 
 let rec apply_undos (n,a,b) =
+  (* Aborts *)
+  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
+  (try Util.repeat a Pfedit.delete_current_proof ()
+   with e -> prerr_endline "WARNING : found a closed environment"; raise e);
   (* Undos *)
   if n<>0 then 
     (prerr_endline ("Applying "^string_of_int n^" undos");
      try Pfedit.undo n
-     with _ -> apply_undos (n,a,BacktrackToNextActiveMark));
-  (* Aborts *)
-  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
-  (try Util.repeat a Pfedit.delete_current_proof ()
-   with e ->
-     begin prerr_endline "WARNING : found a closed environment"; raise e end);
+     with _ -> (* Undo stack exhausted *)
+       apply_backtrack BacktrackToNextActiveMark);
   (* Reset *)
   apply_backtrack b