MAJ V7.3

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

6 files changed, 15 insertions, 9 deletions

diff --git a/doc/README b/doc/README
index b772de3d2..f89d5c607 100755
--- a/doc/README
+++ b/doc/README
@@ -1,7 +1,7 @@
 You can get the whole documentation of Coq in the tar file all-ps-docs.tar.
 
 You can also get separately each document. The documentation of Coq
-V7.2 is divided into the following documents :
+V7.3 is divided into the following documents :
 
      * Tutorial.ps: An introduction to the use of the Coq Proof Assistant;
 
@@ -31,7 +31,7 @@ V7.2 is divided into the following documents :
 
      * Library.ps: A description of the Coq standard library;
 
-     * CHANGES: A description of the differences between version 7.2 
+     * CHANGES: A description of the differences between version 7.3
        and previous versions
 
      * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 3caab62d5..64bae0c43 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -134,7 +134,8 @@ Check half.
 The macro generates also, when it is possible, the projection
 functions for destructuring an object of type {\ident}.
 These projection functions have the same name that the corresponding
-fields. In our example:
+fields. If a field is named ``\verb=_='' then no projection is built for
+this (anonymous) field. In our example:
 
 \begin{coq_example}
 Eval Compute in (top half).
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 602a9a615..9aacb3fda 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -2173,6 +2173,11 @@ every moment.
 
 \item {\tt Print Hint *}\\
   This command displays all declared hints. 
+
+\item {\tt  Print HintDb {\ident} }\\
+\label{PrintHintDb}
+\comindex{Print HintDb}
+ This command displays all hints from database \ident.
 \end{Variants}
 
 
diff --git a/doc/cover.html b/doc/cover.html
index 0d67ef9ed..753fea62d 100644
--- a/doc/cover.html
+++ b/doc/cover.html
@@ -19,15 +19,15 @@
 The Coq Proof Assistant<BR><BR>
  Reference Manual<BR></B></FONT><FONT SIZE=7>
 </FONT>
-<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 7.2</B></FONT><FONT SIZE=5><B>
+<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 7.3</B></FONT><FONT SIZE=5><B>
 </B></FONT><A NAME="text1"></A><A HREF="node.8.html#note1"><SUP><FONT SIZE=2>1</FONT></SUP></A><FONT SIZE=5><B><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
 </B></FONT><FONT SIZE=5><B>The Coq Development Team</B></FONT><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>LogiCal Project</B></FONT><FONT SIZE=5><B><BR><BR><BR>
 </B></FONT></DIV><BR>
 <BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
 
 <DIV ALIGN=left>
-<FONT SIZE=4>V7.2,
-</FONT><BR><FONT SIZE=4>ŠINRIA 1999-2001</FONT><BR></DIV>
+<FONT SIZE=4>V7.3,
+</FONT><BR><FONT SIZE=4>ŠINRIA 1999-2002</FONT><BR></DIV>
 <BR>
 
 
diff --git a/doc/macros.tex b/doc/macros.tex
index f5cfc6193..c70ad240f 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -2,7 +2,7 @@
 % MACROS FOR THE REFERENCE MANUAL OF COQ %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\newcommand{\coqversion}{7.2}
+\newcommand{\coqversion}{7.3}
 
 % For commentaries (define \com as {} for the release manual)
 %\newcommand{\com}[1]{{\it(* #1 *)}}
diff --git a/doc/title.tex b/doc/title.tex
index 9f298a323..3c6b1e484 100755
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -49,9 +49,9 @@ Action ``Types''}
 \vspace*{520pt}
 \thispagestyle{empty}
 \begin{flushleft}
-{\large{V7.2,
+{\large{V7.3,
 \printingdate}}\\[20pt]
-{\large{\copyright INRIA 1999-2001}}\\
+{\large{\copyright INRIA 1999-2002}}\\
 \end{flushleft}
 \newpage}