From af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 9 Dec 2014 12:48:32 +0100
Subject: Switch the few remaining iso-latin-1 files to utf8

---
 doc/RecTutorial/RecTutorial.tex | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'doc/RecTutorial/RecTutorial.tex')

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}).
-- 
cgit v1.2.3