More documentation of new features in CHANGE.

1 files changed, 20 insertions, 8 deletions

diff --git a/CHANGES b/CHANGES
index 9269160dd..2dd953bf3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,7 +40,8 @@ Vernacular commands
   A flag "Set/Unset Record Elimination Schemes" allows to change this.
   The tactic "induction" on a record is now actually doing "destruct".
 - The "Open Scope" command can now be given also a delimiter (e.g. Z).
-- The "Definition" command now allows the "Local" modifier.
+- The "Definition" command now allows the "Local" modifier, allowing
+  for non-importable definitions.
 - The "Let" command can now define local (co)fixpoints.
 - Command "Search" has been renamed into "SearchHead". The command
   name "Search" now behaves like former "SearchAbout". The latter name
@@ -49,13 +50,8 @@ Vernacular commands
   recursively added to the load path, so files from installed libraries
   now need to be fully qualified for the "Require" command to find them.
   The tools/update-require script can be used to convert a development.
-
-Notations
-
-- The syntax "x -> y" is now declared at level 99. In particular, it has
-  now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
-  (possible source of incompatibilities)
-- Notations accept term-providing tactics using the $(...)$ syntax.
+- A new Print Strategies command allows to visualize the opacity status
+  of the whole engine.
 
 Specification Language
 
@@ -68,6 +64,8 @@ Specification Language
 
 Tactics
 
+- New tactic engine allowing real backtrack and multi-success tactics.
+- New "cbn" tactic, a well-behaved simpl.
 - Repeated identical calls to omega should now produce identical proof terms.
 - Tactics btauto, a reflexive boolean tautology solver.
 - Tactic "tauto" was exceptionally able to destruct other connectives
@@ -122,6 +120,10 @@ Program
 
 Notations
 
+- The syntax "x -> y" is now declared at level 99. In particular, it has
+  now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
+  (possible source of incompatibilities)
+- Notations accept term-providing tactics using the $(...)$ syntax.
 - "Bind Scope" can no longer bind "Funclass" and "Sortclass".
 - A notation can be given a (compat "8.x") annotation, making
   it behave like a (only parsing), but flags may active warning
@@ -140,6 +142,16 @@ Tools
   unchanged.)
 - Option -nois prevents coq/theories and coq/plugins to be recursively
   added to the load path. (Same behavior as with coq/user-contrib.)
+- coqdep accepts a -dumpgraph option generating a dot file.
+- Makefiles generated through coq_makefile have three new targets "quick"
+  "checkproof" and "vi2vo", allowing respectively to asynchronously compile
+  the files without playing the proof scripts, asynchronously checking
+  that the quickly generated proofs are correct and generating the object
+  files from the quickly generated proofs.
+
+Interfaces
+
+- CoqIDE uses the new STM machinery, allowing for asynchronous edition.
 
 Internal Infrastructure