aboutsummaryrefslogtreecommitdiff
path: root/doc/Tutorial.tex
diff options
context:
space:
mode:
authorherbelin2002-05-22 11:37:30 +0000
committerherbelin2002-05-22 11:37:30 +0000
commit67947b5d83393f2ab66761b20ab71a8665ce0822 (patch)
treed64c9005d0541a2165eed5f1f44a6bbbd4f7bf42 /doc/Tutorial.tex
parentd7f888afef16ee27b5069f67e146e92a8eb6bf3b (diff)
MAJ V7.3
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8282 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 7de9ad9168..0266f4e55e 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.2:.
+directory \verb:INRIA/coq/V7.3:.
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.2 (January 2002)
+Welcome to Coq 7.3 (May 2002)
Coq <
\end{verbatim}