From c32a1232598efeda80a7b13f504c13a1a4f8a360 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 23 Dec 2001 13:18:05 +0000 Subject: MAJ 7.2 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8263 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/README | 15 +++++++-------- doc/Tutorial.tex | 4 ++-- doc/cover.html | 4 ++-- doc/macros.tex | 2 +- doc/title.tex | 2 +- 5 files changed, 13 insertions(+), 14 deletions(-) diff --git a/doc/README b/doc/README index 5a248ea471..b772de3d20 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.1 is divided into the following documents : +V7.2 is divided into the following documents : * Tutorial.ps: An introduction to the use of the Coq Proof Assistant; @@ -14,16 +14,15 @@ V7.1 is divided into the following documents : - index on tactics, commands and error messages * Reference-Manual-addendum.ps, 75 pp., includes more detailed - explanations and examples about the following topics: + explanations and examples about the following topics: - the extended Cases (C.Cornes) - the Coercions (A. Saļbi) - the tactic Omega (P. Crégut) - - printing proofs in natural language (Y. Coscoy) - - the tactic Ring (S. Boutin and P. Loiseleur) - - the Program tactic (C. Parent) - the Correctness tactic (J.-C. Filliātre) - - the extraction features (J.-C. Filliātre) + - the extraction features (J.-C. Filliātre and P. Letouzey) + - the tactic Ring (S. Boutin and P. Loiseleur) + - the Setoid_replace tactic (C. Renard) Index, page and chapter numbers are shared by the two documents, in order to make cross-references possible. There is also a on the ftp @@ -32,8 +31,8 @@ V7.1 is divided into the following documents : * Library.ps: A description of the Coq standard library; - * CHANGES: A description of the differences between the - versions 6.3.1 and V7.1; + * CHANGES: A description of the differences between version 7.2 + and previous versions * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex index b192e0d0e5..fc22b89bf2 100755 --- a/doc/Tutorial.tex +++ b/doc/Tutorial.tex @@ -32,7 +32,7 @@ he does not use any special interface such as Emacs or Centaur. Instructions on installation procedures, as well as more comprehensive documentation, may be found in the standard distribution of \Coq, which may be obtained by anonymous FTP from site \verb:ftp.inria.fr:, -directory \verb:INRIA/coq/V7.1:. +directory \verb:INRIA/coq/V7.2:. In the following, all examples preceded by the prompting sequence \verb:Coq < : represent user input, terminated by a period. The @@ -46,7 +46,7 @@ The standard invocation of \Coq\ delivers a message such as: \begin{flushleft} \begin{verbatim} unix:~> coqtop -Welcome to Coq 7.1 (September 2001) +Welcome to Coq 7.2 (December 2001) Coq < \end{verbatim} diff --git a/doc/cover.html b/doc/cover.html index b96a099431..0d67ef9ed9 100644 --- a/doc/cover.html +++ b/doc/cover.html @@ -19,14 +19,14 @@ The Coq Proof Assistant

Reference Manual
-


Version 7.1 +


Version 7.2 1










The Coq Development Team
LogiCal Project













-V7.1, +V7.2,
©INRIA 1999-2001

diff --git a/doc/macros.tex b/doc/macros.tex index 9841699ef8..f5cfc61937 100755 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -2,7 +2,7 @@ % MACROS FOR THE REFERENCE MANUAL OF COQ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newcommand{\coqversion}{7.1} +\newcommand{\coqversion}{7.2} % 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 02e02b124e..9f298a3238 100755 --- a/doc/title.tex +++ b/doc/title.tex @@ -49,7 +49,7 @@ Action ``Types''} \vspace*{520pt} \thispagestyle{empty} \begin{flushleft} -{\large{V7.1, +{\large{V7.2, \printingdate}}\\[20pt] {\large{\copyright INRIA 1999-2001}}\\ \end{flushleft} -- cgit v1.2.3