nouvelle MAJ

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

2 files changed, 42 insertions, 30 deletions

diff --git a/ANNONCE b/ANNONCE
index 5e634f2cb8..2493f9cced 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,11 +1,15 @@
-The main features of Coq version 8.1 are
 
-- the implementation of an alternative algorithm for checking the
+It is more than two years since the last release of Coq. We're glad
+to now announce the beta release of Coq version 8.1.
+
+The main features of Coq version 8.1 (beta) are
+
+- the implementation of an auxiliary algorithm for checking the
   convertibility of types, specially dedicated to fast type-checking
   of reflexion-based proofs, and more generally to intensive
   computation
 
-- richer inductive types
+- inductive types
 
   - support for recursively non uniform parameters
   - support for a strong form of sort-polymorphism
@@ -14,14 +18,32 @@ The main features of Coq version 8.1 are
 
   - new implementation of setoid rewrite (contributed by C. Sacerdoti Coen)
   - new implementation of ring (contributed by B. Grégoire and A. Mahboubi)
-  - and several other new tactic features
+  - and several other new tactic features (see attached file CHANGES)
 
-- new libraries
+- libraries
  
   - finite sets and finite maps (by J.-C. Filliâtre and P. Letouzey)
   - strings (by L. Théry)
   - significative extensions of the library on lists
-  - a few other extensions
+  - some other extensions (see attached file CHANGES)
+  - rational numbers (as a quotient over Z/Z+* -- an alternative
+    library based on the canonical Stern-Brocot representation is
+    available in the user contributions)
+
+- experimental features
+
+  - new command to generate proof obligations from definitions of
+    programs required to meet their specification (see chapter 19 of
+    the reference manual)
+
+and many other features mentioned in the CHANGES file.
+
+Most of known bugs have been fixed (see coq-bugs at coq.inria.fr for details).
 
-- improved module system
+Coq version 8.1 hopefully comes with only a few incompatibilities. One
+purpose of this beta version is to estimate to which extent the final
+version 8.1 may provide better support for compatibility.
 
+Coq version 8.1 is based on new Coq version 8.0. Users migrating from
+Coq version 7.x and older must first translate their developments from
+the old syntax using the translator provided with Coq version 8.0.
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
 =============================