MAJ V7.3

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

7 files changed, 37 insertions, 26 deletions

diff --git a/ANNONCE b/ANNONCE
index fcee480f0..6be4886c2 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,19 +1,30 @@
   The Coq development team is pleased to announce the release of Coq
-version 7.2. This release fixes version 7.1 known bugs and offers
-the following novelties or improvements
-
-  - Extension of standard library (sorting; trigonometric, square and square
-    root functions; basic plane geometry; finite sums; more on continuity
-    and derivability; more on min and max; tail-recursive plus and mult)
-  - Extended tactic "Assert H := P" for forward reasoning
-  - Optimised extraction
-  - Coercions allowed in Cases patterns
-  - New declaration "Canonical Structure id = t : I" to help resolution of
-    implicit arguments in developments using Record/Structure
-  - New tactic "ClearBody H" to clear local definition bodies
-
-  Coq V7.2 is available in several formats from http://coq.inria.fr
-and ftp://ftp.inria.fr/INRIA/coq/V7.2. We currently provide the
+version 7.3. This release fixes most of version 7.2 known bugs (see
+http://coq.inria.fr/bin/coq-bugs for the current status of reported
+bugs) and offers the following novelties or improvements.
+
+- New option -dump-glob to coqtop to dump globalizations (to be used by the 
+  new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc).
+- Elimination to Set/Type from empty propositions and to Type from
+  "singleton" propositions now allowed (as a consequence eqT_rec and
+  False_rec are now automatically available).
+- New tactic "Rename x into y" for renaming hypotheses.
+- New tactics "Pose x:=u" and "Pose u" to add definitions to local context.
+- Record's now accept anonymous fields "_" (no projection is built then)
+- Haskell extraction now operational.
+- Extensions of [ZArith]: Zcomplements.v, Zpower.v and Zlogarithms.v
+  have been moved from contrib/omega to ZArith. They now include
+  the Zsgn function, more induction principles (Wf_Z.v and
+  tail of Zcomplements.v) and one more general Euclid theorem.
+
+  Inversion has been improved and Intuition simplified but not in a fully
+compatible way.
+
+  Pcoq user interface (http://www-sop.inria.fr/lemme/pcoq) is not
+ported to V7.3 yet.
+
+  Coq V7.3 is available in several formats from http://coq.inria.fr
+and ftp://ftp.inria.fr/INRIA/coq/V7.3. We currently provide the
 following versions
 
   package for sources
@@ -26,7 +37,7 @@ following versions
   The documentation is available in postscript, pdf and html format.
 
   Please refer to the accompanying document CHANGES or the location
-ftp://ftp.inria.fr/INRIA/coq/V7.2/doc/Changes.html for a full list of
+ftp://ftp.inria.fr/INRIA/coq/V7.3/doc/Changes.html for a full list of
 changes including sources of incompatibilities.
 
   Users are kindly invited to report bugs to coq-bugs@pauillac.inria.fr
diff --git a/INSTALL b/INSTALL
index db08f13a2..bdd9ee43e 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,12 +1,12 @@
 
-            INSTALLATION PROCEDURES FOR THE COQ V7.2 SYSTEM
+            INSTALLATION PROCEDURES FOR THE COQ V7.3 SYSTEM
             -----------------------------------------------
 
 WHAT DO YOU NEED ?
 ==================
 
    Coq is designed to work on computers equipped with the Unix operating 
-   system. In order to compile Coq V7.2 you need:
+   system. In order to compile Coq V7.3 you need:
 
      - Objective Caml version 3.01 or later
        (available at http://caml.inria.fr/)
diff --git a/INSTALL.macosx b/INSTALL.macosx
index fc59dc0b6..0be179c54 100644
--- a/INSTALL.macosx
+++ b/INSTALL.macosx
@@ -1,4 +1,4 @@
-INSTALLATION PROCEDURE FOR THE COQ V7.2 SYSTEM UNDER MACOS X
+INSTALLATION PROCEDURE FOR THE COQ V7.3 SYSTEM UNDER MACOS X
 ------------------------------------------------------------
 
 1) Download compressed archive coq-7.2-Darwin-MacOS-X.tar.gz
diff --git a/README b/README
index d4781f18b..ed9a386c3 100644
--- a/README
+++ b/README
@@ -1,5 +1,5 @@
 
-            		THE COQ V7.2 SYSTEM
+            		THE COQ V7.3 SYSTEM
             		===================
 
 INSTALLATION.
@@ -11,7 +11,7 @@ INSTALLATION.
 DOCUMENTATION.
 ==============
 
-   The documentation of Coq V7.2 is available by anonymous ftp (see below),
+   The documentation of Coq V7.3 is 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/configure b/configure
index 7b6e290eb..a960aa446 100755
--- a/configure
+++ b/configure
@@ -6,9 +6,9 @@
 # 
 ##################################
 
-VERSION=7.2
+VERSION=7.3
 VERSIONSI=1.0
-DATE="January 2002"
+DATE="May 2002"
 
 # a local which command for sh
 which () {
diff --git a/distrib/RH/coq.spec.tpl b/distrib/RH/coq.spec.tpl
index 31d49d185..6266e4f66 100644
--- a/distrib/RH/coq.spec.tpl
+++ b/distrib/RH/coq.spec.tpl
@@ -1,12 +1,12 @@
 Name: coq
-Version: 7.2
+Version: 7.3
 Release: 1
 Summary: The Coq Proof Assistant
 Copyright: freely redistributable
 Group: Applications/Math
 Vendor: INRIA Rocquencourt
 URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V7.2/coq-7.2.tar.gz
+Source: ftp://ftp.inria.fr/INRIA/coq/V7.3/coq-7.3.tar.gz
 Icon: petit-coq.gif
 
 %description
diff --git a/library/library.ml b/library/library.ml
index bba4ae35c..47beca5f3 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -220,7 +220,7 @@ let module_segment = function
 
 let module_full_filename m = (find_module m).module_filename
 
-let vo_magic_number = 0702 (* V7.2 *)
+let vo_magic_number = 0703 (* V7.3 *)
 
 let (raw_extern_module, raw_intern_module) =
   System.raw_extern_intern vo_magic_number ".vo"