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

4 files changed, 17 insertions, 17 deletions

diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index 0d727e1702..d0884be0dd 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 6fb7534d53..2a2c211963 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 26064e8644..caee81782c 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 11dde2cd51..438f2133d4 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},