aboutsummaryrefslogtreecommitdiff
path: root/doc/Tutorial.tex
diff options
context:
space:
mode:
authorherbelin2001-12-23 13:18:05 +0000
committerherbelin2001-12-23 13:18:05 +0000
commitc32a1232598efeda80a7b13f504c13a1a4f8a360 (patch)
treedd4d194bfceb254852cb7690bcf7e372d22bb9cb /doc/Tutorial.tex
parente0f4ef6c39d77f9c7dcb1f7e91432c92ccd4bc42 (diff)
MAJ 7.2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8263 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Tutorial.tex')
-rwxr-xr-xdoc/Tutorial.tex4
1 files changed, 2 insertions, 2 deletions
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}