Switch the few remaining iso-latin-1 files to utf8

10 files changed, 98 insertions, 100 deletions

diff --git a/doc/LICENSE b/doc/LICENSE
index 990874803..ada22e669 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -8,7 +8,7 @@ forth in the Open Publication License, v1.0 or later (the latest
 version is presently available at http://www.opencontent.org/openpub/).
 Options A and B are *not* elected.
 
-The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
+The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
 Paulin-Mohring. All documents (the LaTeX source and the PostScript,
 PDF and html outputs) are copyright (c) INRIA 1999-2006. The material
 connected to the Coq Tutorial may be distributed only subject to the
@@ -25,7 +25,7 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA
 distributed under the terms of the Lesser General Public License
 version 2.1 or later. 
 
-The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
+The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
 Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All
 documents (the LaTeX source and the PostScript, PDF and html outputs)
 are copyright (c) INRIA 2004-2006. The material connected to the FAQ
@@ -36,7 +36,7 @@ http://www.opencontent.org/openpub/). Options A and B are *not*
 elected.
 
 The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
-Castéran and Eduardo Gimenez. All related documents (the LaTeX and
+Castéran and Eduardo Gimenez. All related documents (the LaTeX and
 BibTeX sources and the PostScript, PDF and html outputs) are copyright
 (c) INRIA 1997-2006. The material connected to the Tutorial on
 [Co-]Inductive Types in Coq may be distributed only subject to the
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index 0d727e170..d0884be0d 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -19,7 +19,7 @@ Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}}
 % \newcommand{\refmancite}[1]{\cite{coqrefman}}
 % \newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}}
 
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{makeidx}
 % \usepackage{multind}
@@ -1007,7 +1007,7 @@ The following commented examples will show the different situations to consider.
 %q_r\;({c}_i\;x_1\;\ldots x_n)$$ for dependent one. In the
 %following section, we illustrate this general scheme for different
 %recursive types.
-%%\textbf{A vérifier}
+%%\textbf{A vérifier}
 
 \subsubsection{The Empty Type}
 
@@ -1505,7 +1505,7 @@ definition of the notions of \emph{positivity condition} and
 %arguments of its own introduction rules, in the sense on the following
 %definition:
 
-%\textbf{La définition du manuel de référence est plus complexe:
+%\textbf{La définition du manuel de référence est plus complexe:
 %la recopier ou donner seulement des exemples?
 %}
 %\begin{enumerate}
@@ -1718,7 +1718,7 @@ Inductive ex_Prop  (P : Prop {\arrow} Prop) : Prop :=
 %*)
 %\end{alltt}
 
-% \textbf{Et par ça?
+% \textbf{Et par ça?
 %}
 
 Notice that predicativity on sort \citecoq{Set} forbids us to build
@@ -2300,8 +2300,8 @@ Qed.
 \begin{exercise}
 Consider the following language of arithmetic expression, and 
 its operational semantics, described by a set of rewriting rules.
-%\textbf{J'ai enlevé une règle de commutativité de l'addition qui 
-%me paraissait bizarre du point de vue de la sémantique opérationnelle}
+%\textbf{J'ai enlevé une règle de commutativité de l'addition qui 
+%me paraissait bizarre du point de vue de la sémantique opérationnelle}
 
 \begin{alltt}
 Inductive ArithExp : Set :=
@@ -3150,7 +3150,7 @@ Qed.
 It is interesting to look at another proof of 
 \citecoq{vector0\_is\_vnil}, which illustrates a technique developed
 and used by various people (consult in the \emph{Coq-club} mailing
-list archive the contributions by Yves Bertot, Pierre Letouzey, Laurent Théry,
+list archive the contributions by Yves Bertot, Pierre Letouzey, Laurent Théry,
 Jean Duprat, and Nicolas Magaud, Venanzio Capretta and Conor McBride).
 This technique is also used for unfolding  infinite list definitions
 (see chapter13 of~\cite{coqart}).
diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex
index 6fb7534d5..2a2c21196 100644
--- a/doc/RecTutorial/coqartmacros.tex
+++ b/doc/RecTutorial/coqartmacros.tex
@@ -46,8 +46,8 @@
 \renewcommand{\marginpar}[1]{}
 
 \addtocounter{secnumdepth}{1}
-\providecommand{\og}{«}
-\providecommand{\fg}{»}
+\providecommand{\og}{«}
+\providecommand{\fg}{»}
 
 
 \newcommand{\hard}{\mbox{\small *}}
diff --git a/doc/RecTutorial/manbiblio.bib b/doc/RecTutorial/manbiblio.bib
index 26064e864..caee81782 100644
--- a/doc/RecTutorial/manbiblio.bib
+++ b/doc/RecTutorial/manbiblio.bib
@@ -4,11 +4,11 @@
 
 @TECHREPORT{RefManCoq,
         AUTHOR             = {Bruno~Barras, Samuel~Boutin,
-  Cristina~Cornes, Judicaël~Courant, Yann~Coscoy, David~Delahaye,
-  Daniel~de~Rauglaudre, Jean-Christophe~Filliâtre, Eduardo~Giménez,
-  Hugo~Herbelin, Gérard~Huet, Henri~Laulhère, César~Muñoz,
+  Cristina~Cornes, Judicaël~Courant, Yann~Coscoy, David~Delahaye,
+  Daniel~de~Rauglaudre, Jean-Christophe~Filliâtre, Eduardo~Giménez,
+  Hugo~Herbelin, Gérard~Huet, Henri~Laulhère, César~Muñoz,
   Chetan~Murthy, Catherine~Parent-Vigouroux, Patrick~Loiseleur,
-  Christine~Paulin-Mohring, Amokrane~Saïbi, Benjamin~Werner},
+  Christine~Paulin-Mohring, Amokrane~Saïbi, Benjamin~Werner},
         INSTITUTION        = {INRIA},
         TITLE              = {{The Coq Proof Assistant Reference Manual -- Version V6.2}},
         YEAR               = {1998}
@@ -461,9 +461,9 @@ of the {ML} language},
   title = {The {Coq} Proof Assistant - A tutorial, Version 6.1},
   institution = {INRIA},
   type = {rapport technique},
-  month = {Août},
+  month = {Août},
   year = {1997},
-  note = {Version révisée distribuée avec {Coq}},
+  note = {Version révisée distribuée avec {Coq}},
   number = {204},
 }
 
diff --git a/doc/RecTutorial/morebib.bib b/doc/RecTutorial/morebib.bib
index 11dde2cd5..438f2133d 100644
--- a/doc/RecTutorial/morebib.bib
+++ b/doc/RecTutorial/morebib.bib
@@ -1,14 +1,14 @@
 @book{coqart,
    title = "Interactive Theorem Proving and Program Development. 
     Coq'Art: The Calculus of Inductive Constructions",
-   author = "Yves Bertot and Pierre Castéran",
+   author = {Yves Bertot and Pierre Castéran},
    publisher = "Springer Verlag",
    series = "Texts in Theoretical Computer Science. An EATCS series",  
  year = 2004
 }
 
 @Article{Coquand:Huet,
-  author = 	 {Thierry Coquand and Gérard Huet},
+  author = 	 {Thierry Coquand and Gérard Huet},
   title = 	 {The Calculus of Constructions},
   journal = 	 {Information and Computation},
   year = 	 {1988},
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 647a151d7..5a6691072 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -14,7 +14,7 @@
 %\usepackage{multicol}
 \usepackage{hevea}
 \usepackage{fullpage}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[english]{babel}
 
 \ifpdf   % si on est en pdflatex
@@ -138,7 +138,7 @@
   \large(\protect\ref{lastquestion}
   \ Hints)
 }
-\author{Pierre Castéran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux}
+\author{Pierre Castéran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux}
 \maketitle
 
 %%%%%%%
@@ -254,7 +254,7 @@ notes~\cite{Types:Dowek}.
 \item[Inductive types]
 Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}.
 \item[Co-Inductive types]
-Eduardo Giménez' thesis~\cite{EGThese}.
+Eduardo Giménez' thesis~\cite{EGThese}.
 \item[Miscellaneous] A
 \ahref{http://coq.inria.fr/doc/biblio.html}{bibliography} about Coq
 \end{description}
@@ -397,7 +397,7 @@ New versions of {\Coq} are announced on the coq-club mailing list. If you only w
 
 \Question{Is there any book about {\Coq}?}
 
-The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004:
+The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004:
 \begin{quote}
 ``This book provides a pragmatic introduction to the development of
 proofs and certified programs using \Coq. With its large collection of
@@ -1124,7 +1124,7 @@ Qed.
 Just use the semi-decision tactic: \firstorder.
 
 \iffalse
-todo: demander un exemple à Pierre
+todo: demander un exemple à Pierre
 \fi
 
 \Question{My goal is solvable by a sequence of rewrites, how can I prove it?}
@@ -1200,7 +1200,7 @@ Qed.
 
 \Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?}
 
-You need the {\gb} tactic (see Loïc Pottier's homepage).
+You need the {\gb} tactic (see Loïc Pottier's homepage).
 
 \subsection{Tactics usage}
 
@@ -1265,7 +1265,7 @@ You can split your hint bases into smaller ones.
 
 \Question{What is the equivalent of {\tauto} for classical logic?}
 
-Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation.
+Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation.
 
 
 \Question{I want to replace some term with another in the goal, how can I do it?}
@@ -1914,7 +1914,7 @@ Notation "x ^2" := (Rmult x x) (at level 20).
 \end{verbatim}
 Note that you can not use:
 \begin{tt}
-Notation "x $^²$" := (Rmult x x) (at level 20).
+Notation "x $^2$" := (Rmult x x) (at level 20).
 \end{tt}
 because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8.
 
diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
index d41ab7f09..4d90efcdb 100644
--- a/doc/faq/fk.bib
+++ b/doc/faq/fk.bib
@@ -16,11 +16,11 @@
 }
 
 @PHDTHESIS{EGThese,
-  author = {Eduardo Giménez},
+  author = {Eduardo Giménez},
   title = {Un Calcul de Constructions Infinies et son application
-a la vérification de systèmes communicants},
-  type = {thèse d'Université},
-  school = {Ecole Normale Supérieure de Lyon},
+a la vérification de systèmes communicants},
+  type = {thèse d'Université},
+  school = {Ecole Normale Supérieure de Lyon},
   month = {December},
   year = {1996},
 }
@@ -29,7 +29,7 @@ a la vérification de systèmes communicants},
 %%%%%%% Semantique %%%%%%%
 
 @misc{Sem:cours,
-  author = "François Pottier",
+  author = "François Pottier",
   title =  "{Typage et Programmation}",
   year = "2002",
   howpublished = "Lecture notes",
@@ -109,7 +109,7 @@ year = {1981}
 @book{Coq:coqart,
   title = "Interactive Theorem Proving and Program Development,
 	  Coq'Art: The Calculus of Inductive Constructions",
-  author = "Yves Bertot and Pierre Castéran",
+  author = "Yves Bertot and Pierre Castéran",
   publisher = "Springer Verlag",
   series = "Texts in Theoretical Computer Science. An
 	  EATCS series",
@@ -118,8 +118,8 @@ year = {1981}
 			 
 @phdthesis{Coq:Del01,
 	AUTHOR = "David Delahaye",
-	TITLE = "Conception de langages pour décrire les preuves et les 
-                  automatisations dans les outils d'aide à la preuve",
+	TITLE = "Conception de langages pour décrire les preuves et les 
+                  automatisations dans les outils d'aide à la preuve",
 	SCHOOL = {Universit\'e Paris~6},
 	YEAR = "2001",
         Type = {Th\`ese de Doctorat}
@@ -133,7 +133,7 @@ year = {1981}
     url = "citeseer.nj.nec.com/gimenez98tutorial.html" }
 
 @phdthesis{Coq:Mun97,
-	AUTHOR = "César Mu{\~{n}}oz",
+	AUTHOR = "César Mu{\~{n}}oz",
 	TITLE = "Un calcul de substitutions pour la repr\'esentation
                   de preuves partielles en th\'eorie de types",
 	SCHOOL = {Universit\'e Paris~7},
@@ -191,7 +191,7 @@ year = {1981}
 }
 
 @misc{PVS-Tactics:cours,
-  author = "César Muñoz",
+  author = "César Muñoz",
   title = "Strategies in {PVS}",
   howpublished = "Lecture notes",
   note = "National Institute of Aerospace",
@@ -288,9 +288,9 @@ year = {1981}
 }
 
 @TECHREPORT{modelpa2000,
-  AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg 
+  AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg 
                   and J.-F. Monin and C. Paulin and A. Petit and D. Rouillard},
-  TITLE = {Automates temporisés CALIFE},
+  TITLE = {Automates temporisés CALIFE},
   INSTITUTION = {Calife},
   YEAR = 2000,
   URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F1.1.ps.gz},
@@ -298,8 +298,8 @@ year = {1981}
 }
 
 @TECHREPORT{CaFrPaRo2000,
-  AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard},
-  TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions              et les p-automates},
+  AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard},
+  TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions              et les p-automates},
   INSTITUTION = {Calife},
   YEAR = 2000,
   URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F5.4.ps.gz},
@@ -335,7 +335,7 @@ year = {1981}
   MONTH = JAN,
   SCHOOL = {{Paris 7}},
   TITLE = {Extraction de programmes dans le {Calcul des Constructions}},
-  TYPE = {Thèse d'université},
+  TYPE = {Thèse d'université},
   YEAR = {1989},
   URL = {http://www.lri.fr/~paulin/these.ps.gz}
 }
@@ -427,11 +427,11 @@ nd Applications},
 
 @PHDTHESIS{Pau96b,
   AUTHOR = {Christine Paulin-Mohring},
-  TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur},
-  SCHOOL = {Université Claude Bernard Lyon I},
+  TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur},
+  SCHOOL = {Université Claude Bernard Lyon I},
   YEAR = 1996,
   MONTH = DEC,
-  TYPE = {Habilitation à diriger les recherches},
+  TYPE = {Habilitation à diriger les recherches},
   URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
 }
 
@@ -488,7 +488,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
 }
 
 @TECHREPORT{kmu2002rr,
-  AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain},
+  AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain},
   TITLE = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria},
   INSTITUTION = {LRI},
   YEAR = 2002,
@@ -509,7 +509,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
 }
 
 @INPROCEEDINGS{contejean03wst,
-  AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain},
+  AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain},
   TITLE = {{Proving Termination of Rewriting with {\sc C\textit{i}ME}}},
   CROSSREF = {wst03},
   PAGES = {71--73},
@@ -661,7 +661,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
   YEAR = {2003},
   EDITOR = {Albert Rubio},
   MONTH = JUN,
-  NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain}
+  NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain}
 }
 
 @INPROCEEDINGS{FilliatreLetouzey03,
@@ -740,8 +740,8 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
 
 @INPROCEEDINGS{Filliatre01a,
   AUTHOR = {J.-C. Filli\^atre},
-  TITLE = {La supériorité de l'ordre supérieur},
-  BOOKTITLE = {Journées Francophones des Langages Applicatifs},
+  TITLE = {La supériorité de l'ordre supérieur},
+  BOOKTITLE = {Journées Francophones des Langages Applicatifs},
   PAGES = {15--26},
   MONTH = {Janvier},
   YEAR = 2002,
@@ -749,18 +749,18 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
   URL = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz},
   CODE = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps},
   ABSTRACT = {
-  Nous présentons ici une écriture fonctionnelle de l'algorithme de
+  Nous présentons ici une écriture fonctionnelle de l'algorithme de
   Koda-Ruskey, un algorithme pour engendrer une large famille
   de codes de Gray. En s'inspirant de techniques de programmation par
-  continuation, nous aboutissons à un code de neuf lignes seulement,
-  bien plus élégant que les implantations purement impératives
-  proposées jusqu'ici, notamment par Knuth. Dans un second temps,
-  nous montrons comment notre code peut être légèrement modifié pour
-  aboutir à une version de complexité optimale.
-  Notre implantation en Objective Caml rivalise d'efficacité avec les
-  meilleurs codes C. Nous détaillons les calculs de complexité,
-  un exercice intéressant en présence d'ordre supérieur et d'effets de
-  bord combinés.}
+  continuation, nous aboutissons à un code de neuf lignes seulement,
+  bien plus élégant que les implantations purement impératives
+  proposées jusqu'ici, notamment par Knuth. Dans un second temps,
+  nous montrons comment notre code peut être légèrement modifié pour
+  aboutir à une version de complexité optimale.
+  Notre implantation en Objective Caml rivalise d'efficacité avec les
+  meilleurs codes C. Nous détaillons les calculs de complexité,
+  un exercice intéressant en présence d'ordre supérieur et d'effets de
+  bord combinés.}
 }
 
 @TECHREPORT{Filliatre00c,
@@ -901,33 +901,33 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
   YEAR = 1999,
   MONTH = {July},
   URL = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz},
-  ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant
-  traits impératifs et fonctionnels dans le cadre de la théorie des
+  ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant
+  traits impératifs et fonctionnels dans le cadre de la théorie des
   types.
 
-  La théorie des types constitue un puissant langage de spécification,
-  naturellement adapté à la preuve de programmes purement
-  fonctionnels.  Pour y certifier également des programmes impératifs,
-  nous commençons par exprimer leur sémantique de manière purement
+  La théorie des types constitue un puissant langage de spécification,
+  naturellement adapté à la preuve de programmes purement
+  fonctionnels.  Pour y certifier également des programmes impératifs,
+  nous commençons par exprimer leur sémantique de manière purement
   fonctionnelle. Cette traduction repose sur une analyse statique des
   effets de bord des programmes, et sur l'utilisation de la notion de
-  monade, notion que nous raffinons en l'associant à la notion d'effet
-  de manière générale.  Nous montrons que cette traduction est
-  sémantiquement correcte.
-
-  Puis, à partir d'un programme annoté, nous construisons une preuve
-  de sa spécification, traduite de manière fonctionnelle. Cette preuve
-  est bâtie sur la traduction fonctionnelle précédemment
-  introduite. Elle est presque toujours incomplète, les parties
-  manquantes étant autant d'obligations de preuve qui seront laissées
-  à la charge de l'utilisateur.  Nous montrons que la validité de ces
-  obligations entraîne la correction totale du programme.
-
-  Nous avons implanté notre travail dans l'assistant de preuve
-  Coq, avec lequel il est dès à présent distribué. Cette
-  implantation se présente sous la forme d'une tactique prenant en
-  argument un programme annoté et engendrant les obligations de
-  preuve.  Plusieurs algorithmes non triviaux ont été certifiés à
+  monade, notion que nous raffinons en l'associant à la notion d'effet
+  de manière générale.  Nous montrons que cette traduction est
+  sémantiquement correcte.
+
+  Puis, à partir d'un programme annoté, nous construisons une preuve
+  de sa spécification, traduite de manière fonctionnelle. Cette preuve
+  est bâtie sur la traduction fonctionnelle précédemment
+  introduite. Elle est presque toujours incomplète, les parties
+  manquantes étant autant d'obligations de preuve qui seront laissées
+  à la charge de l'utilisateur.  Nous montrons que la validité de ces
+  obligations entraîne la correction totale du programme.
+
+  Nous avons implanté notre travail dans l'assistant de preuve
+  Coq, avec lequel il est dès à présent distribué. Cette
+  implantation se présente sous la forme d'une tactique prenant en
+  argument un programme annoté et engendrant les obligations de
+  preuve.  Plusieurs algorithmes non triviaux ont été certifiés à
   l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de
   Knuth-Morris-Pratt).}
 }
@@ -1081,7 +1081,7 @@ tique},
 }
 
 @InCollection{cc,
-  author =       {Thierry Coquand and Gérard Huet},
+  author =       {Thierry Coquand and Gérard Huet},
   title =        {The Calculus of Constructions},
   booktitle =    {Information and Computation},
   year =         {1988},
@@ -1095,7 +1095,7 @@ tique},
   title =        {Inductively defined types},
   booktitle =    {Proceedings of Colog'88},
   year =         {1990},
-  editor =       {P. Martin-Löf and G. Mints},
+  editor =       {P. Martin-Löf and G. Mints},
   volume =       {417},
   series =       {LNCS},
   publisher = {Springer-Verlag}
@@ -1318,7 +1318,7 @@ s},
 }
 
 @INPROCEEDINGS{CoHu85a,
-        AUTHOR             = {Thierry Coquand and Gérard Huet},
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
         ADDRESS            = {Linz},
         BOOKTITLE          = {EUROCAL'85},
         PUBLISHER          = SV,
@@ -1329,7 +1329,7 @@ s},
 }
 
 @INPROCEEDINGS{CoHu85b,
-        AUTHOR             = {Thierry Coquand and Gérard Huet},
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
         BOOKTITLE          = {Logic Colloquium'85},
         EDITOR             = {The Paris Logic Group},
         PUBLISHER          = {North-Holland},
@@ -1338,7 +1338,7 @@ s},
 }
 
 @ARTICLE{CoHu86,
-        AUTHOR             = {Thierry Coquand and Gérard Huet},
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
         JOURNAL            = {Information and Computation},
         NUMBER             = {2/3},
         TITLE              = {The {Calculus of Constructions}},
@@ -2092,7 +2092,7 @@ the Calculus of Inductive Constructions}},
 @PHDTHESIS{Bar99,
         AUTHOR             = {B. Barras},
         SCHOOL             = {Universit\'e Paris 7},
-        TITLE              = {Auto-validation d'un système de preuves avec familles inductives},
+        TITLE              = {Auto-validation d'un système de preuves avec familles inductives},
         TYPE               = {Th\`ese de Doctorat},
         YEAR               = {1999}
 }
@@ -2177,7 +2177,7 @@ Decomposition}},
 
 
 @Book{CoqArt,
-  author =	 {Yves bertot and Pierre Castéran},
+  author =	 {Yves bertot and Pierre Castéran},
   title = 	 {Coq'Art},
   publisher = 	 {Springer-Verlag},
   year = 	 2004,
diff --git a/doc/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex
index d881329a6..ac1686c25 100644
--- a/doc/rt/RefMan-cover.tex
+++ b/doc/rt/RefMan-cover.tex
@@ -1,6 +1,5 @@
 \documentstyle[RRcover]{book}
-        % L'utilisation du style `french' force le résumé français à
-        % apparaître en premier.
+        % The use of the style `french' forces the french abstract to appear first.
 
 \RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1}
 \RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1
@@ -26,7 +25,7 @@ Amokrane Sa{\"\i}bi, Benjamin Werner}
 v\'erification de preuves formelles dans une logique d'ordre
 sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
 Ce document constitue le manuel de r\'ef\'erence de la version V7.1
-qui est distribu\'ee par ftp anonyme à l'adresse
+qui est distribu\'ee par ftp anonyme \`a l'adresse
 \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles,
diff --git a/doc/rt/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex
index b747b812e..aefea8d42 100644
--- a/doc/rt/Tutorial-cover.tex
+++ b/doc/rt/Tutorial-cover.tex
@@ -1,6 +1,5 @@
 \documentstyle[RRcover]{book}
-        % L'utilisation du style `french' force le résumé français à
-        % apparaître en premier.
+        % The use of the style `french' forces the french abstract to appear first.
 \RRetitle{
 The Coq Proof Assistant \\ A Tutorial \\ Version 7.1
 \thanks{This research was partly supported by ESPRIT Basic Research
@@ -29,7 +28,7 @@ Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNR
 v\'erification de preuves formelles dans une logique d'ordre
 sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
 Ce document constitue une introduction pratique \`a l'utilisation de
-la version V7.1 qui est distribu\'ee par ftp anonyme à l'adresse
+la version V7.1 qui est distribu\'ee par ftp anonyme \`a l'adresse
 \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index de3d9c3f2..836944ab1 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