diff options
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/stdlib/Library.tex | 2 | ||||
| -rwxr-xr-x | doc/tutorial/Tutorial.tex | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 9260e7e189..8735bc720f 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,7 +3,7 @@ \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} -\usepackage{coqdoc} +\usepackage{../../coqdoc} \input{../common/version} \input{../common/title} 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} |