nouvelle MAJ

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

1 files changed, 13 insertions, 23 deletions

diff --git a/CHANGES b/CHANGES
index b0945ed0cc..f6e75bfd37 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,16 +9,11 @@ Logic
 Syntax
 
 - No more support for version 7 syntax and for translation to version 8 syntax.
-- Support for primitive interpretation of string literals
-- Extended support for Unicode ranges (Unicode doc TODO)
 - In fixpoints, the { struct ... } annotation is not mandatory any more when 
   only one of the arguments has an inductive type (doc TODO) 
-
-Environment variables
-
-- COQREMOTEBROWSER to set the command invoked to start the remote browser
-  both in Coq and coqide. Standard syntax: "%s" is the placeholder for the
-  URL (doc TODO)
+- Added disjunctive patterns in match-with patterns
+- Support for primitive interpretation of string literals
+- Extended support for Unicode ranges (Unicode doc TODO)
 
 Vernacular commands
 
@@ -31,10 +26,6 @@ Vernacular commands
 - New command "Whelp" to send requests to the Helm database of proofs
   formalized in the Calculus of Inductive Constructions
 
-Gallina
-
-- Added disjunctive patterns in match-with patterns
-
 Ltac
 
 - New primitive "external" for communication with tool external to Coq
@@ -105,14 +96,12 @@ Tactics
      swap H asks you to prove A from hypothesis B 
   * revert : revert H is generalize H; clear H
 
-
 Extraction
  
 - all type parts should now disappear instead of sometimes producing _ 
   (for instance in Map.empty).
 - TODO bug fixes...
 
-
 Modules
 
 - Added "Locate Module qualid" to get the full path of a module.
@@ -134,10 +123,12 @@ Notations
 
 Libraries
 
+- New library on String and Ascii characters (contributed by L. Thery)
+- New library FSets+FMaps of finite sets and maps (TODO doc quelque part)
+- New library QArith on rational numbers
 - Small extension of Zmin.V, new Zmax.v, new Zminmax.v
 - Reworking of the files on classical logic and description principles
   (possible incompatibilities)
-- New library on String and Ascii characters (contributed by L. Thery)
 - Few other improvements in ZArith potentially exceptionally breaking the
   compatibility (useless hypothesys of Zgt_square_simpl and
   Zlt_square_simpl removed; fixed names mentioning letter O instead of
@@ -145,21 +136,16 @@ Libraries
 - Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
 - Znumtheory now contains a gcd function that can compute within Coq
 - More lemmas stated on Type in Wf.v, removal of redundant Fix_F
+- Change of the internal names of lemmas in OmegaLemmas
 - Coq.List.In_dec has been set transparent (this may exceptionally break
   proof scripts, set it locally opaque for compatibility)
-- Change of the internal names of lemmas in OmegaLemmas
+- More on permutations of lists in List.v and Permutation.v (TODO en dire plus ?)
 - List.v has been much expanded (TODO en dire plus)
-- The notion of permutation of lists has been developped, both in 
-  List.v and Permutation.v (TODO en dire plus ?)
 - New file SetoidList.v now contains results about lists seen with 
   respect to a setoid equality. 
 - Library NArith has been expanded, mostly with results coming from 
   Intmap (for instance a bitwise xor), plus also a bridge between N and 
   Bitvector. 
-- A new library FSets+FMaps of finite sets and maps (TODO doc quelque part)
-  Nota: files FSetAVL and FMapAVL in this library are known to take some 
-  time to compile. On slow computers, you may choose to disable them 
-  via the Configure option --fsets no 
 - Intmap has been reorganized. In particular its address type "addr" is 
   now N. User contributions known to use Intmap have been adapted 
   accordingly. If you're using this library please contact us. 
@@ -170,9 +156,13 @@ Libraries
 
 Tools
 
-- New semantics for coqtop options ("-batch" expects option "-top dir"
+- new semantics for coqtop options ("-batch" expects option "-top dir"
   for loading vernac file that contains definitions).
 - coq_makefile now removes custom targets that are file names in "make clean"
+- new environment variable COQREMOTEBROWSER to set the command invoked
+  to start the remote browser both in Coq and coqide. Standard syntax:
+  "%s" is the placeholder for the URL (doc TODO)
+
 
 Changes from V8.0beta to V8.0
 =============================