From dd507b21f2125c460c8c8462a485bf56a0d04c73 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 16 May 2002 15:49:49 +0000
Subject: MAJ V7.3
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8280 85f007b7-540e-0410-9357-904b9bb8a0f7
---
doc/README | 4 ++--
doc/RefMan-ext.tex | 3 ++-
doc/RefMan-tac.tex | 5 +++++
doc/cover.html | 6 +++---
doc/macros.tex | 2 +-
doc/title.tex | 4 ++--
6 files changed, 15 insertions(+), 9 deletions(-)
diff --git a/doc/README b/doc/README
index b772de3d20..f89d5c6070 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 3caab62d5e..64bae0c436 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 602a9a615e..9aacb3fda0 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 0d67ef9ed9..753fea62dc 100644
--- a/doc/cover.html
+++ b/doc/cover.html
@@ -19,15 +19,15 @@
The Coq Proof Assistant
Reference Manual
-
Version 7.2
+
Version 7.3
1
The Coq Development Team
LogiCal Project
-V7.2,
-
ŠINRIA 1999-2001
+V7.3,
+
ŠINRIA 1999-2002
diff --git a/doc/macros.tex b/doc/macros.tex
index f5cfc61937..c70ad240f4 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 9f298a3238..3c6b1e484a 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}
--
cgit v1.2.3