MAJ V7.3

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

1 files changed, 9 insertions, 4 deletions

diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index cba07eb7f..e9ec07d91 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -316,8 +316,8 @@ Christine Paulin
 The version V7 is a new implementation started in September 1999 by
 Jean-Christophe Filliâtre. This is a major revision with respect to
 the internal architecture of the system.  The \Coq{} version 7.0 was
-distributed in march 2001, version 7.1 in september 2001 and version
-7.2 in january 2002.
+distributed in March 2001, version 7.1 in September 2001, version
+7.2 in January 2002 and version 7.3 in May 2002.
 
 Jean-Christophe Filliâtre designed the architecture of the new system, he
 introduced a new representation for environments and wrote a new kernel
@@ -344,12 +344,14 @@ trigonometric functions, square, square roots, finite sums, Chasles
 property and basic plane geometry.
 
 Jean-Christophe Filliâtre and Pierre Letouzey redesigned a new
-extraction procedure from Coq terms to Caml programs. This new
+extraction procedure from Coq terms to Caml or Haskell programs. This new
 extraction procedure, unlike the one implemented in previous version
 of \Coq{} is able to handle all terms in the Calculus of Inductive
 Constructions, even involving universes and strong elimination. P.
 Letouzey adapted user contributions to extract ML programs when it was
 sensible.
+Jean-Christophe Filliâtre wrote \verb=coqdoc=, a documentation
+tool for Coq libraries usable from version 7.2.
 
 Bruno Barras improved the reduction algorithms efficiency and
 the confidence level in the correctness of Coq critical type-checking
@@ -361,6 +363,9 @@ Yves Bertot designed  the \texttt{SearchPattern} and
 
 Micaela Mayero and David Delahaye introduced a decision tactic for commutative fields.
 
+Christine Paulin changed the elimination rules for empty and singleton
+propositional inductive types.
+
 Loïc Pottier developed a tactic solving linear inequalities on real numbers.
 
 Pierre Crégut developed a new version based on reflexion of the Omega
@@ -384,7 +389,7 @@ Intensive users suggested improvements of the system :
 Y. Bertot, L. Pottier, L. Théry , P. Zimmerman from INRIA 
 C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D.
 \begin{flushright}
-Orsay, Jan. 2002\\
+Orsay, May. 2002\\
 Hugo Herbelin \& Christine Paulin
 \end{flushright}
 \newpage