MAJ

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

5 files changed, 13 insertions, 18 deletions

diff --git a/ANNONCE b/ANNONCE
index c9ff7c49b..a3138749f 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -17,8 +17,7 @@ quantification and notations for standard arithmetical notions
 (e.g. +, *, <, <=) without conflicts with the rest of the syntax. A new
 notion of "interpretation scopes" allows also to reuse the same
 notations in different contexts of formalisation (e.g. +, * are valid
-on nat, Z, R, types, etc). The new syntax, with explanatory examples,
-is described in document ??? from the distribution.
+on nat, Z, R, types, etc).
 
   Thirdly, the standard library has been revised and simplified. There
 is now only one equality "=" and one existential quantification valid
@@ -27,9 +26,8 @@ been re-organised. The basic notions from the initial state now have
 implicit arguments.
 
   Coq version 8.0 comes with a smart and robust comment-preserving
-automatic translator from old to new syntax. Follow the instructions
-in document ??? from the distribution to update your developments from
-old to new syntax.
+automatic translator from old to new syntax. A translation package
+with a documentation of the new syntax accompanies the distribution.
 
   Coq version 8.0 brings also a new automation tactic for first-order
 statements and various improvements of existing tactics.
@@ -48,7 +46,9 @@ on http://www.labri.fr/~casteran/CoqArt.
 
   The sources of Coq V8.0 beta, including its integrated development
 environment, are available from http://coq.inria.fr/ and
-ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/.
+ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/. The translation
+package coq-8.0beta-translator.tar.gz is available separately at
+the same location.
 
   Please refer to the accompanying document CHANGES or the location
 ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/doc/Changes.html for a
@@ -57,11 +57,6 @@ full list of changes including sources of incompatibilities.
   The (at the time partial) documentation of Coq V8.0 is available in
 postscript, pdf and html format.
 
-# Si on a le temps...
-  Notice that you can browse the new standard library at
-http://coq.inria.fr/library-eng.html (these pages have been generated
-by coqdoc).
-
   Users are kindly invited to report bugs at http://coq.inria.fr/bin/coq-bugs
 and to mail Coq-Club@pauillac.inria.fr for general questions or remarks.
 Note that you can now choose your personal options at
diff --git a/INSTALL b/INSTALL
index 72c4d2fdc..e411d0efe 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,12 +1,12 @@
 
-            INSTALLATION PROCEDURES FOR THE COQ V7.4 SYSTEM
+            INSTALLATION PROCEDURES FOR THE COQ V8.0 SYSTEM
             -----------------------------------------------
 
 WHAT DO YOU NEED ?
 ==================
 
    Coq is designed to work on computers equipped with the Unix operating 
-   system. In order to compile Coq V7.4 you need:
+   system. In order to compile Coq V8.0 you need:
 
      - Objective Caml version 3.06 or later
        (available at http://caml.inria.fr/)
@@ -49,7 +49,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
    you do not have to check this point anymore.
 
 3- The uncompression and un-tarring of the distribution file gave birth 
-   to a directory named "coq-7.xx". You can rename this directory and put 
+   to a directory named "coq-8.xx". You can rename this directory and put 
    it wherever you want. Just keep in mind that you will need some spare
    space during the compilation (reckon on about 50 Mb of disk space
    for the whole system in native-code compilation). Once installed, the
diff --git a/README b/README
index 671ccd426..fc127e192 100644
--- a/README
+++ b/README
@@ -1,5 +1,5 @@
 
-            		THE COQ V7.4 SYSTEM
+            		THE COQ V8.0 SYSTEM
             		===================
 
 INSTALLATION.
@@ -11,7 +11,7 @@ INSTALLATION.
 DOCUMENTATION.
 ==============
 
-   The documentation of Coq V7.4 is available by anonymous ftp (see below),
+   The documentation of Coq V8.0 available by anonymous ftp (see below),
    in a directory doc/. The documents are available separately or
    all together in the tar file all-docs.tar .
 
diff --git a/README.win b/README.win
index dba76dfd0..4d698e93b 100644
--- a/README.win
+++ b/README.win
@@ -1,4 +1,4 @@
-THE COQ V7.4 SYSTEM
+THE COQ V8.0 SYSTEM
 ===================
 
     This file contains remarks specific to the windows port of Coq.
diff --git a/configure b/configure
index 3a282c673..7663092cc 100755
--- a/configure
+++ b/configure
@@ -8,7 +8,7 @@
 
 VERSION=8.0beta
 VERSIONSI=1.0
-DATE="Nov 2003"
+DATE="Dec 2003"
 
 # a local which command for sh
 which () {