aboutsummaryrefslogtreecommitdiff
path: root/doc/tutorial/Tutorial.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tutorial/Tutorial.tex')
-rwxr-xr-xdoc/tutorial/Tutorial.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index de3d9c3f2e..836944ab1c 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -1,6 +1,6 @@
\documentclass[11pt,a4paper]{book}
\usepackage[T1]{fontenc}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage{pslatex}
@@ -11,7 +11,7 @@
%\makeindex
\begin{document}
-\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring}{}
+\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring}{}
%\tableofcontents
@@ -30,7 +30,7 @@ manner a tutorial on the basic specification language, called Gallina,
in which formal axiomatisations may be developed, and on the main
proof tools. For more advanced information, the reader could refer to
the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y.
-Bertot and P. Castéran on practical uses of the \Coq{} system.
+Bertot and P. Castéran on practical uses of the \Coq{} system.
Coq can be used from a standard teletype-like shell window but
preferably through the graphical user interface