Documentation of last commit concerning Backtracking

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

1 files changed, 15 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index a12caacba2..b38a346a04 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,15 +1,30 @@
 Changes from V8.4
 =================
 
+Vernacular commands
+
+- Undo and UndoTo are now handling the proof states. They may
+  perform some extra steps of backtrack to avoid states where
+  the proof state is unavailable (typically a closed proof).
+- The commands Suspend and Resume have been removed.
+- A basic Show Script has been reintroduced (no indentation).
+
 Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
 
 Program
+
 - "Solve Obligations using" changed to "Solve Obligations with",
   consistent with "Proof with".
 - Program Lemma, Definition now respect automatic introduction.
 
+CoqIDE
+
+- Coqide now supports the Restart command, and Undo (with a warning).
+  Better support for Abort.
+
+
 Changes from V8.4beta to V8.4
 =============================