aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Tutorial.tex
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-02-03 09:25:40 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-02-03 09:25:40 +0000
commit108e617657082fcd1d2fa4acba657681ac9df3e8 (patch)
treee9d55cca34d9707bcebd875123e7a18fb7c32db8 /doc/Tutorial.tex
parent2fa44bb507d977d6cefda5435687c7d1bec70735 (diff)
version 7.4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8318 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 0266f4e55..7d408e57a 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.3:.
+directory \verb:INRIA/coq/V7.4:.
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.3 (May 2002)
+Welcome to Coq 7.4 (Feb 2003)
Coq <
\end{verbatim}