diff options
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/README | 15 | ||||
| -rwxr-xr-x | doc/Tutorial.tex | 4 | ||||
| -rw-r--r-- | doc/cover.html | 4 | ||||
| -rwxr-xr-x | doc/macros.tex | 2 | ||||
| -rwxr-xr-x | doc/title.tex | 2 |
5 files changed, 13 insertions, 14 deletions
diff --git a/doc/README b/doc/README index 5a248ea47..b772de3d2 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 b192e0d0e..fc22b89bf 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 b96a09943..0d67ef9ed 100644 --- a/doc/cover.html +++ b/doc/cover.html @@ -19,14 +19,14 @@ 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.1</B></FONT><FONT SIZE=5><B> +<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 7.2</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.1, +<FONT SIZE=4>V7.2, </FONT><BR><FONT SIZE=4>©INRIA 1999-2001</FONT><BR></DIV> <BR> diff --git a/doc/macros.tex b/doc/macros.tex index 9841699ef..f5cfc6193 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 02e02b124..9f298a323 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} |