MAJ V7.1

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

1 files changed, 45 insertions, 44 deletions

diff --git a/ANNONCE b/ANNONCE
index a8b4eeef26..0f336dac40 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,55 +1,56 @@
+  The Coq development team is pleased to release version 7.1 of Coq.
+This release is a major update on version 6.3.1 and a bug-fixes update
+on version 7.0.
 
-  The LogiCal team (ex-Coq team) is releasing a new version of Coq
-(V7.0). The new features are:
+  The main features of Coq versions 7.0 and 7.1 on version 6.3.1 are
 
   - a primitive let-in construct
-  - qualified names (such as Logic.f_equal)
-  - a more high-level tactic language based on a small functional core with
-    recursors and elaborated matching operators for terms and proof contexts
-    (by David Delahaye)
-  - an improved Search facilities using patterns (by Yves Bertot)
-  - a "natural" syntax for real numbers (by Micaela Mayero)
-  - a new implementation of the extraction from Coq proofs to Ocaml programs
-    (by J.-C. Filliātre and P. Letouzey)
-  - an improved reduction strategy for lazy evaluation (by B. Barras)
-  - various bug fixes
-  - a command to export theories to XML to be used with Helm's publishing
-    and rendering tools (see http://www.cs.unibo.it/helm) (by Claudio
-    Sacerdoti Coen)
-
-  The Realizer/Program tactics are not available in Coq V7.0.
+  - qualified names
+  - library structuration
+  - a high-level tactic language
+  - improved search facilities
+  - export of theories to XML for publishing and rendering purposes
+  - a deep restructuration of the code (safer, simpler and more efficient)
+  - 
+
+  Compared to version 7.0, the new version provides with
+
+  - port of user contributions (including new libraries for
+    constructive complex analysis, floating-point numbers, P-automaton
+    and graph theory, and formalizations of the ABR algorithm, CTL and
+    TCTL temporal logic, the Railroad Crossing Problem, a subset of the
+    C language, imperative Bresenham line drawing algorithm, imperative
+    Marché's minimal edition distance algorithm, Buchberger's algorithm,
+    RSA cryptographic algorithm, Stalmarck tautology checker algorithm,
+    the Fundamental Theorem of Algebra and ZFC set theory).
+  - new tactics NewDestruct, NewInduction and Assert intended to
+    improve the behaviour of previous Elim and Induction, Case and
+    Destruct, and Cut tactics
+  - known-bugs fixes
+  - excessive memory use mainly fixed
+
+  The Realizer/Program tactics are not available in Coq V7.1.
   The Correctness command can be used instead.
 
-  The internals of Coq have changed a lot and this justifies the new
-major version number 7 though the differences are small for end-users
-The internals of Coq will continue to change significantly in the next
-months and we recommend tactic developers to take contact with us for
-adapting their code.
+  Coq V7.1 is available in several formats from http://coq.inria.fr
+and ftp://ftp.inria.fr/INRIA/coq/V7.1. We currently provide the
+following versions
 
-  Coq V7.0 is available in several formats from http://coq.inria.fr 
-and ftp://ftp.inria.fr/INRIA/coq/V7. 
-  We currently provide the following versions
+  package for sources
+  rpm package for sources
+  rpm package for linux
+  binary package for Sun-Solaris
+  binary version for Windows
+  binary version for MacOS X (without specific GUI)
 
-	package for sources
-	rpm package for sources
-	rpm package for linux
-	binary package for Sun-Solaris
-	binary version for Windows
+  The documentation is available in postscript, pdf and html format.
 
-	No binary package is provided for MacOS.
+  Please refer to the accompanying document CHANGES for a full
+list of changes including sources of incompatibilities.
 
-  The documentation has been updated and is available in postscript, 
-pdf and html format.
+  Users are kindly invited to report bugs to coq-bugs@pauillac.inria.fr
+and to mail Coq-Club@pauillac.inria.fr for general questions or
+remarks (moderated).
 
-  User's contributions are not yet available
-
-  Please refer to the accompanying document Changes.dvi for a full
-list of changes including sources of incompatibilities (very few).
-
-  Users are kindly invited to provide feedback on the new features by
-mailing to coq-bugs@pauillac.inria.fr for bug reports or to
-Coq-Club@pauillac.inria.fr for general questions or remarks
-(moderated).
-
-	The Coq development team
+  The Coq development team (in LogiCal team)