From 4aa0debbae28fa5768d2ce3f9ffe82d2a015ce39 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 23 Mar 2012 16:49:54 +0000
Subject: Documentation of last commit concerning Backtracking

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15086 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'CHANGES')

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
 =============================
 
-- 
cgit v1.2.3