diff options
| author | Pierre Letouzey | 2014-12-09 12:48:32 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-12-09 14:27:21 +0100 |
| commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
| tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /doc/RecTutorial/RecTutorial.tex | |
| parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) | |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'doc/RecTutorial/RecTutorial.tex')
| -rw-r--r-- | doc/RecTutorial/RecTutorial.tex | 14 |
1 files changed, 7 insertions, 7 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}). |
