aboutsummaryrefslogtreecommitdiff
path: root/doc/Tutorial.tex
diff options
context:
space:
mode:
authorherbelin2001-09-24 20:34:25 +0000
committerherbelin2001-09-24 20:34:25 +0000
commit5cf95106d590fc6bd393c71db2b57179983b2d27 (patch)
treee5a662a51ef2ced747f41219a0d39e28319775e0 /doc/Tutorial.tex
parent15e6ecfb6fee27d926cdd2f59bda4531b8ed3879 (diff)
Mise en place avertissements pour rep�rer les erreurs volontaires de coq-tex
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8226 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 dd5b0ff5f7..b192e0d0e5 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.0:.
+directory \verb:INRIA/coq/V7.1:.
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.0 (April 2001)
+Welcome to Coq 7.1 (September 2001)
Coq <
\end{verbatim}