aboutsummaryrefslogtreecommitdiff
path: root/doc/tutorial/Tutorial.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tutorial/Tutorial.tex')
-rwxr-xr-xdoc/tutorial/Tutorial.tex8
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 6e913e7319..cbe130a60d 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -59,7 +59,7 @@ invocation of \Coq\ delivers a message such as:
\begin{flushleft}
\begin{verbatim}
unix:~> coqtop
-Welcome to Coq 8.0 (Mar 2004)
+Welcome to Coq trunk (Jun. 2008)
Coq <
\end{verbatim}
@@ -67,9 +67,9 @@ Coq <
\end{small}
The first line gives a banner stating the precise version of \Coq~
-used. You should always return this banner when you report an
-anomaly to our hot-line \verb:coq-bugs@pauillac.inria.fr: or on our
-bug-tracking system~:\verb|http://logical.futurs.inria.fr/coq-bugs|
+used. You should always return this banner when you report an anomaly
+to our bug-tracking system
+\verb|http://logical.futurs.inria.fr/coq-bugs|
\chapter{Basic Predicate Calculus}