aboutsummaryrefslogtreecommitdiff
path: root/doc/Tutorial.tex
diff options
context:
space:
mode:
authorfilliatr2000-12-15 10:22:46 +0000
committerfilliatr2000-12-15 10:22:46 +0000
commit2ccb521cf21c1db3d3c49cc547cb446f54f49dd6 (patch)
treefd9c93be1de3887d342f1651dcf3f0117f4bb1b8 /doc/Tutorial.tex
parent4e283e52a29ba769b4b18fd26145924a40b21ec6 (diff)
config avec autoconf
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8146 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 a2459384cf..d554675f1b 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/V6.3.1:.
+directory \verb:INRIA/coq/V7.0:.
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 V6.3.1 (December 1999)
+Welcome to Coq 7.0 (November 2000)
Coq <
\end{verbatim}