From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 CHANGES | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 54 insertions(+), 2 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 74aefe49..c245fb25 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,54 @@
-Changes from V8.3 to V8.4
-=========================
+Changes from V8.4beta to 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).
+- New command "Set Parsing Explicit" for deactivating parsing (and printing)
+  of implicit arguments (useful for teaching).
+- New command "Grab Existential Variables" to transform the unresolved evars at
+  the end of a proof into goals.
+
+Tactics
+
+- Still no general "info" tactical, but new specific tactics
+  info_auto, info_eauto, info_trivial which provides information
+  on the proofs found by auto/eauto/trivial. Display of these
+  details could also be activated by Set Info Auto/Eauto/Trivial.
+- Details on everything tried by auto/eauto/trivial during
+  a proof search could be obtained by "debug auto", "debug eauto",
+  "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
+- New command "r string" that interprets "idtac string" as a breakpoint
+  and jumps to its next use in Ltac debugger.
+- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
+  harvey, zenon, gwhy) have been removed, since Why2 has not been
+  maintained for the last few years. The Why3 plugin should be a suitable
+  replacement in most cases.
+
+Libraries
+
+- MSetRBT : a new implementation of MSets via Red-Black trees (initial
+  contribution by Andrew Appel).
+- MSetAVL : for maximal sharing with the new MSetRBT, the argument order
+  of Node has changed (this should be transparent to regular MSets users). 
+
+Module System
+
+- The names of modules (and module types) are now in a fully separated
+  namespace from ordinary definitions : "Definition E:=0. Module E. End E."
+  is now accepted.
+
+CoqIDE
+
+- Coqide now supports the Restart command, and Undo (with a warning).
+  Better support for Abort.
+
+Changes from V8.3 to V8.4beta
+=============================
 
 Logic
 
@@ -69,6 +118,8 @@ Tactics
 - When applying destruct or inversion on a fixpoint hiding an inductive
   type, recursive calls to the fixpoint now remain folded by default (rare
   source of incompatibility generally solvable by adding a call to simpl).
+- The behavior of the simpl tactic can be tuned using the new "Arguments"
+  vernacular.
 
 Vernacular commands
 
@@ -90,6 +141,7 @@ Vernacular commands
   to avoid conversion at Qed time to go into a very long computation.
 - New command "Show Goal ident" to display the statement of a goal, even
   a closed one (available from Proof General).
+- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope".
 
 Module System
 
-- 
cgit v1.2.3