CoqIDE: 2 problèmes de undo encore:

- dans le "replay", l'état n'était pas correctement sauvegardé d'où une
  perte d'efficacité en cas de rejeux répétés,
- bug de synchronisation dans le calcul de la pile des lemmes ouverts.

+ réajout de la variante standard de Set Printing All dans le menu display.



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

1 files changed, 5 insertions, 4 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 6208fba373..918519b1a0 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -23,25 +23,26 @@ type printing_state = {
   mutable printing_no_notation : bool;
   mutable printing_all : bool;
   mutable printing_evar_instances : bool;
-  mutable printing_universes : bool
+  mutable printing_universes : bool;
+  mutable printing_full_all : bool
 }
 
 val printing_state : printing_state
 
 type reset_mark =
   | ResetToId of Names.identifier
-  | ResetToState of  Libnames.object_name
+  | ResetToState of Libnames.object_name
 
 type reset_status =
   | NoReset
   | ResetAtSegmentStart of Names.identifier
   | ResetAtRegisteredObject of reset_mark
 
-type undo_info = int * int
+type undo_info = identifier list
 
 val undo_info : unit -> undo_info
 
-type reset_info = reset_status * bool ref
+type reset_info = reset_status * undo_info * bool ref
 
 val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit