16 files changed, 80 insertions, 80 deletions

diff --git a/doc/common/styles/html/coqremote/styles.hva b/doc/common/styles/html/coqremote/styles.hva
index 413f3bf62..94fb0d38b 100644
--- a/doc/common/styles/html/coqremote/styles.hva
+++ b/doc/common/styles/html/coqremote/styles.hva
@@ -1,6 +1,6 @@
 \renewcommand{\@meta}{
 \begin{rawhtml}
-<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" />
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
 <link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" />
 <link type="text/css" rel="stylesheet" media="all" href="/modules/node/node.css" />
 <link type="text/css" rel="stylesheet" media="all" href="/modules/system/defaults.css" />
diff --git a/doc/common/styles/html/simple/styles.hva b/doc/common/styles/html/simple/styles.hva
index 64cf21067..71c4ffedf 100644
--- a/doc/common/styles/html/simple/styles.hva
+++ b/doc/common/styles/html/simple/styles.hva
@@ -1,6 +1,6 @@
 \renewcommand{\@meta}{
 \begin{rawhtml}
-<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" />
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
 
 <link rel="stylesheet" type="text/css" href="style.css" />
 <link rel="stylesheet" type="text/css" href="coqdoc.css" />
diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
index 461e8e6d0..eee41a679 100644
--- a/doc/refman/AddRefMan-pre.tex
+++ b/doc/refman/AddRefMan-pre.tex
@@ -18,15 +18,15 @@ Manual.
   and Hugo Herbelin.
 
 \item[Implicit coercions] This chapter details the use of the coercion
-  mechanism.  It is contributed by Amokrane Saïbi.
+  mechanism.  It is contributed by Amokrane Saïbi.
 
 %\item[Proof of imperative programs] This chapter explains how to
 %  prove properties of annotated programs with imperative features.
-%  It is contributed by Jean-Christophe Filliâtre
+%  It is contributed by Jean-Christophe Filliâtre
 
 \item[Program extraction] This chapter explains how to extract in practice ML
   files from $\FW$ terms.   It is contributed by Jean-Christophe
-  Filliâtre and Pierre Letouzey.
+  Filliâtre and Pierre Letouzey.
 
 \item[Program] This chapter explains the use of the \texttt{Program}
   vernacular which allows the development of certified
@@ -37,7 +37,7 @@ Manual.
 %  manual of the tools he wrote for printing proofs in natural
 %  language. At this time, French and English languages are supported.
 
-\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole
+\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole
   class of arithmetic problems.
 
 \item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This
@@ -46,7 +46,7 @@ Manual.
 
 \item[The {\tt Setoid\_replace} tactic] This is a
   tactic to do rewriting on types equipped with specific (only partially
-  substitutive) equality. The chapter is contributed by Clément Renard.
+  substitutive) equality. The chapter is contributed by Clément Renard.
 
 \item[Calling external provers] This chapter describes several tactics
   which call external provers.
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index dcff7fb8d..60b4b2241 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -1,5 +1,5 @@
 \achapter{Implicit Coercions}
-\aauthor{Amokrane Saïbi}
+\aauthor{Amokrane Saïbi}
 
 \label{Coercions-full}
 \index{Coercions!presentation}
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 37326c10f..86c16f635 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -1,6 +1,6 @@
 \achapter{Extraction of programs in Objective Caml and Haskell}
 \label{Extraction}
-\aauthor{Jean-Christophe Filliâtre and Pierre Letouzey}
+\aauthor{Jean-Christophe Filliâtre and Pierre Letouzey}
 \index{Extraction}
 
 We present here the \Coq\ extraction commands, used to build certified
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 2e4a8059e..4a4fab153 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -1,5 +1,5 @@
 \achapter{Micromega : tactics for solving arithmetic goals over ordered rings}
-\aauthor{Frédéric Besson and Evgeny Makarov}
+\aauthor{Frédéric Besson and Evgeny Makarov}
 \newtheorem{theorem}{Theorem}
 
  
diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
index 3ecc7e652..70e36a5ee 100644
--- a/doc/refman/Nsatz.tex
+++ b/doc/refman/Nsatz.tex
@@ -1,5 +1,5 @@
 \achapter{Nsatz: tactics for proving equalities in integral domains}
-\aauthor{Loïc Pottier}
+\aauthor{Loïc Pottier}
 
 The tactic \texttt{nsatz} proves goals of the form
 
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex
index b946d03b7..1610305e7 100644
--- a/doc/refman/Omega.tex
+++ b/doc/refman/Omega.tex
@@ -1,6 +1,6 @@
 \achapter{Omega: a solver of quantifier-free problems in
 Presburger Arithmetic}
-\aauthor{Pierre Crégut}
+\aauthor{Pierre Crégut}
 \label{OmegaChapter}
 
 \asection{Description of {\tt omega}}
@@ -94,7 +94,7 @@ is generated:
 
 \end{ErrMsgs}
 
-%% Ce code est débranché pour l'instant
+%% This code is currently unplugged
 %% 
 % \asubsection{Control over the output}
 % There are some flags that can be set to get more information on the procedure
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index b0c328a54..1cce48b95 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -39,10 +39,10 @@ The remaining sections are concerned with the type-checking of terms.
 The beginner can skip them.
 
 The reader seeking a background on the Calculus of Inductive
-Constructions may read several papers. Giménez and Castéran~\cite{GimCas05} 
+Constructions may read several papers. Giménez and Castéran~\cite{GimCas05}
 provide
 an introduction to inductive and co-inductive definitions in Coq. In
-their book~\cite{CoqArt}, Bertot and Castéran give a precise
+their book~\cite{CoqArt}, Bertot and Castéran give a precise
 description of the \CIC{} based on numerous practical examples.
 Barras~\cite{Bar99}, Werner~\cite{Wer94} and
 Paulin-Mohring~\cite{Moh97} are the most recent theses dealing with
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index 4ef5818aa..dac3c60bd 100644
--- a/doc/refman/RefMan-coi.tex
+++ b/doc/refman/RefMan-coi.tex
@@ -184,7 +184,7 @@ Eval compute in (tl nat (from 0)).
 $(\from\;n)\equiv(\cons\;\nat\;n\;(\from \; (\S\;n)))$
 does not hold as definitional one. Nevertheless, it can be proved 
 as a propositional  equality, in the sense of Leibniz's equality. 
-The version {\it à la Leibniz} of the equality above follows from 
+The version {\it à la Leibniz} of the equality above follows from
 a general lemma stating that eliminating and then re-introducing a stream
 yields the same stream.
 \begin{coq_example}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 51aba9570..6eca9fc4c 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -918,7 +918,7 @@ section is closed.
 %However, a name already used in a closed section (see \ref{Section})
 %can be reused. In this case, the old name is no longer accessible.
 
-% Obsolète
+% Obsolète
 %\item A module implicitly open a section. Be careful not to name a
 %module with an identifier already used in the module (see \ref{compiled}).
 \end{Remarks}
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 5f1e11c47..49382f3e2 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -485,7 +485,7 @@ Inductive sumor (A:Set) (B:Prop) : Set :=
 | inright (_:B).
 \end{coq_example*}
 
-We may define variants of the axiom of choice, like in Martin-Löf's
+We may define variants of the axiom of choice, like in Martin-Löf's
 Intuitionistic Type Theory.
 \ttindex{Choice}
 \ttindex{Choice2}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 23d4ee10d..91823c4a4 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -194,7 +194,7 @@ predicates''.
 
 \begin{flushright}
 Rocquencourt, Feb. 1st 1995\\
-Gérard Huet
+Gérard Huet
 \end{flushright}
 
 \section*{Credits: addendum for version 6.1}
@@ -211,7 +211,7 @@ Cristina Cornes designed an extension of the \Coq{} syntax to allow
 definition of terms using a powerful pattern-matching analysis in the
 style of ML programs.
 
-Amokrane Saïbi wrote a mechanism to simulate
+Amokrane Saïbi wrote a mechanism to simulate
 inheritance between types families extending a proposal by Peter
 Aczel. He also developed a mechanism to automatically compute which
 arguments of a constant may be inferred by the system and consequently
@@ -228,7 +228,7 @@ rings using a canonical set of rewriting rules and equality modulo
 associativity and commutativity. 
 
 Finally the organisation of the \Coq{} distribution has been supervised
-by Jean-Christophe Filliâtre with the help of Judicaël Courant
+by Jean-Christophe Filliâtre with the help of Judicaël Courant
 and Bruno Barras.
 
 \begin{flushright}
@@ -249,7 +249,7 @@ these changes is a faster parsing procedure with greatly improved
 syntax-error messages. The user-interface to introduce grammar or
 pretty-printing rules has also changed.
 
-Eduardo Giménez redesigned the internal 
+Eduardo Giménez redesigned the internal
 tactic libraries, giving uniform names 
 to Caml functions corresponding to \Coq{} tactic names. 
 
@@ -260,7 +260,7 @@ specification language: the definitions by fixpoints and
 pattern-matching have a more readable syntax.  Patrick Loiseleur
 introduced user-friendly notations for arithmetic expressions.
 
-New tactics were introduced: Eduardo Giménez improved a mechanism to
+New tactics were introduced: Eduardo Giménez improved a mechanism to
 introduce macros for tactics, and designed special tactics for
 (co)inductive definitions; Patrick Loiseleur designed a tactic to
 simplify polynomial expressions in an arbitrary commutative ring which
@@ -271,12 +271,12 @@ using a proof term with holes as a proof scheme.
 David Delahaye designed the \textsf{SearchIsos} tool to search an
 object in the library given its type (up to isomorphism).
 
-Henri Laulhère produced the \Coq{} distribution for the Windows environment. 
+Henri Laulhère produced the \Coq{} distribution for the Windows environment.
 
 Finally, Hugo Herbelin was the main coordinator of the \Coq{}
 documentation with principal contributions by Bruno Barras, David Delahaye, 
 Jean-Christophe Filli\^atre, Eduardo
-Giménez, Hugo Herbelin and Patrick Loiseleur. 
+Giménez, Hugo Herbelin and Patrick Loiseleur.
 
 \begin{flushright}
 Orsay, May 4th 1998\\
@@ -315,13 +315,13 @@ Christine Paulin
 \section*{Credits: versions 7}
 
 The version V7 is a new implementation started in September 1999 by
-Jean-Christophe Filliâtre. This is a major revision with respect to
+Jean-Christophe Filliâtre. This is a major revision with respect to
 the internal architecture of the system.  The \Coq{} version 7.0 was
 distributed in March 2001, version 7.1 in September 2001, version
 7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in
 February 2003.
 
-Jean-Christophe Filliâtre designed the architecture of the new system, he
+Jean-Christophe Filliâtre designed the architecture of the new system, he
 introduced a new representation for environments and wrote a new kernel
 for type-checking terms. His approach was to use functional
 data-structures in order to get more sharing, to prepare the addition
@@ -345,7 +345,7 @@ Olivier Desmettre extended this library with axiomatic
 trigonometric functions, square, square roots, finite sums, Chasles
 property and basic plane geometry.
 
-Jean-Christophe Filliâtre and Pierre Letouzey redesigned a new
+Jean-Christophe Filliâtre and Pierre Letouzey redesigned a new
 extraction procedure from \Coq{} terms to \textsc{Caml} or
 \textsc{Haskell} programs. This new 
 extraction procedure, unlike the one implemented in previous version
@@ -353,7 +353,7 @@ of \Coq{} is able to handle all terms in the Calculus of Inductive
 Constructions, even involving universes and strong elimination. P.
 Letouzey adapted user contributions to extract ML programs when it was
 sensible.
-Jean-Christophe Filliâtre wrote \verb=coqdoc=, a documentation
+Jean-Christophe Filliâtre wrote \verb=coqdoc=, a documentation
 tool for {\Coq} libraries usable from version 7.2.
 
 Bruno Barras improved the reduction algorithms efficiency and
@@ -369,9 +369,9 @@ Micaela Mayero and David Delahaye introduced {\tt Field}, a decision tactic for
 Christine Paulin changed the elimination rules for empty and singleton
 propositional inductive types.
 
-Loïc Pottier developed {\tt Fourier}, a tactic solving linear inequalities on real numbers.
+Loïc Pottier developed {\tt Fourier}, a tactic solving linear inequalities on real numbers.
 
-Pierre Crégut developed a new version based on reflexion of the {\tt Omega}
+Pierre Crégut developed a new version based on reflexion of the {\tt Omega}
 decision tactic.
 
 Claudio Sacerdoti Coen designed an XML output for the {\Coq}
@@ -385,21 +385,21 @@ Pierre Courtieu developed a command and a tactic to reason on the
 inductive structure of recursively defined functions.
 
 Jacek Chrz\k{a}szcz designed and implemented the module system of
-{\Coq} whose foundations are in Judicaël Courant's PhD thesis.
+{\Coq} whose foundations are in Judicaël Courant's PhD thesis.
 
 \bigskip
 
 The development was coordinated by C. Paulin.
 
-Many discussions within the Démons team and the LogiCal project
+Many discussions within the Démons team and the LogiCal project
 influenced significantly the design of {\Coq} especially with 
 %J. Chrz\k{a}szcz, P. Courtieu, 
 J. Courant, J. Duprat, J. Goubault, A. Miquel,
-C. Marché, B. Monate and B. Werner.
+C. Marché, B. Monate and B. Werner.
 
-Intensive users suggested improvements of the system : 
-Y. Bertot, L. Pottier, L. Théry, P. Zimmerman from INRIA, 
-C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D.
+Intensive users suggested improvements of the system :
+Y. Bertot, L. Pottier, L. Théry, P. Zimmerman from INRIA,
+C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D.
 \begin{flushright}
 Orsay, May. 2002\\
 Hugo Herbelin \& Christine Paulin
@@ -489,16 +489,16 @@ types. He is also the maintainer of the non-domain specific automation
 tactics.
 
 Benjamin Monate is the developer of the \CoqIDE{} graphical
-interface with contributions by Jean-Christophe Filliâtre, Pierre
-Letouzey, Claude Marché and Bruno Barras.
+interface with contributions by Jean-Christophe Filliâtre, Pierre
+Letouzey, Claude Marché and Bruno Barras.
 
-Claude Marché coordinated the edition of the Reference Manual for
+Claude Marché coordinated the edition of the Reference Manual for
  \Coq{} V8.0.
 
 Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
 extraction tool and module system of {\Coq}.
 
-Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and 
+Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin ando
 contributors from Sophia-Antipolis and Nijmegen participated to the
 extension of the library.
 
@@ -518,7 +518,7 @@ Hugo Herbelin \& Christine Paulin\\
 
 {\Coq} version 8.1 adds various new functionalities.
 
-Benjamin Grégoire implemented an alternative algorithm to check the
+Benjamin Grégoire implemented an alternative algorithm to check the
 convertibility of terms in the {\Coq} type-checker. This alternative
 algorithm works by compilation to an efficient bytecode that is
 interpreted in an abstract machine similar to Xavier Leroy's ZINC
@@ -537,11 +537,11 @@ arbitrary transition systems.
 
 Claudio Sacerdoti Coen added new features to the module system. 
 
-Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new
+Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new
 more efficient and more general simplification algorithm on rings and
 semi-rings.
 
-Laurent Théry and Bruno Barras developed a new significantly more efficient
+Laurent Théry and Bruno Barras developed a new significantly more efficient
 simplification algorithm on fields.
 
 Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
@@ -550,7 +550,7 @@ Claudio Sacerdoti Coen added new tactic features.
 Hugo Herbelin implemented matching on disjunctive patterns.
 
 New mechanisms made easier the communication between {\Coq} and external
-provers. Nicolas Ayache and Jean-Christophe Filliâtre implemented
+provers. Nicolas Ayache and Jean-Christophe Filliâtre implemented
 connections with the provers {\sc cvcl}, {\sc Simplify} and {\sc
 zenon}. Hugo Herbelin implemented an experimental protocol for calling
 external tools from the tactic language.
@@ -561,10 +561,10 @@ to specify the behavior of programs with subtypes.
 A mechanism to automatically use some specific tactic to solve
 unresolved implicit has been implemented by Hugo Herbelin.
 
-Laurent Théry's contribution on strings and Pierre Letouzey and
-Jean-Christophe Filliâtre's contribution on finite maps have been
+Laurent Théry's contribution on strings and Pierre Letouzey and
+Jean-Christophe Filliâtre's contribution on finite maps have been
 integrated to the {\Coq} standard library. Pierre Letouzey developed a
-library about finite sets ``à la {\ocaml}''. With Jean-Marc
+library about finite sets ``à la {\ocaml}''. With Jean-Marc
 Notin, he extended the library on lists. Pierre Letouzey's
 contribution on rational numbers has been integrated and extended..
 
@@ -578,7 +578,7 @@ reason on the inductive structure of recursively defined functions.
 Jean-Marc Notin significantly contributed to the general maintenance
 of the system. He also took care of {\textsf{coqdoc}}.
 
-Pierre Castéran contributed to the documentation of (co-)inductive
+Pierre Castéran contributed to the documentation of (co-)inductive
 types and suggested improvements to the libraries.
 
 Pierre Corbineau implemented a declarative mathematical proof
@@ -611,7 +611,7 @@ rewriting on arbitrary transitive relations.
 
 Another major improvement of Coq 8.2 is the evolution of the
 arithmetic libraries and of the tools associated to them. Benjamin
-Grégoire and Laurent Théry contributed a modular library for building
+Grégoire and Laurent Théry contributed a modular library for building
 arbitrarily large integers from bounded integers while Evgeny Makarov
 contributed a modular library of abstract natural and integer
 arithmetics together with a few convenient tactics. On his side,
@@ -619,7 +619,7 @@ Pierre Letouzey made numerous extensions to the arithmetic libraries on
 $\mathbb{Z}$ and $\mathbb{Q}$, including extra support for
 automatization in presence of various number-theory concepts.
 
-Frédéric Besson contributed a reflexive tactic based on
+Frédéric Besson contributed a reflexive tactic based on
 Krivine-Stengle Positivstellensatz (the easy way) for validating
 provability of systems of inequalities. The platform is flexible enough
 to support the validation of any algorithm able to produce a
@@ -630,7 +630,7 @@ $\mathbb{Z}$) and sum-of-squares (for non-linear systems).  Evgeny
 Makarov made the platform generic over arbitrary ordered rings.
 
 Arnaud Spiwack developed a library of 31-bits machine integers and,
-relying on Benjamin Grégoire and Laurent Théry's library, delivered a
+relying on Benjamin Grégoire and Laurent Théry's library, delivered a
 library of unbounded integers in base $2^{31}$. As importantly, he
 developed a notion of ``retro-knowledge'' so as to safely extend the
 kernel-located bytecode-based efficient evaluation algorithm of Coq
@@ -649,7 +649,7 @@ better support for proof or definition by fixpoint, more expressive
 rewriting tactics, better support for meta-variables, more convenient
 notations, ...
 
-Élie Soubiran improved the module system, adding new features (such as
+Élie Soubiran improved the module system, adding new features (such as
 an ``include'' command) and making it more flexible and more
 general. He and Pierre Letouzey improved the support for modules in
 the extraction mechanism.
@@ -658,7 +658,7 @@ Matthieu Sozeau extended the \textsc{Russell} language, ending in an
 convenient way to write programs of given specifications, Pierre
 Corbineau extended the Mathematical Proof Language and the
 automatization tools that accompany it, Pierre Letouzey supervised and
-extended various parts the standard library, Stéphane Glondu
+extended various parts the standard library, Stéphane Glondu
 contributed a few tactics and improvements, Jean-Marc Notin provided
 help in debugging, general maintenance and {\tt coqdoc} support,
 Vincent Siles contributed extensions of the {\tt Scheme} command and
@@ -669,7 +669,7 @@ type-checker that can be used to certify {\tt .vo} files. Especially,
 as this verifier runs in a separate process, it is granted not to be
 ``hijacked'' by virtually malicious extensions added to {\Coq}.
 
-Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and
+Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and
 Julien Forest acted as maintainers of features they implemented in
 previous versions of Coq.
 
@@ -681,7 +681,7 @@ Mimram, he also helped making Coq compatible with recent software
 tools.  Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to
 improved the libraries of integers, rational, and real numbers. We
 also thank many users and partners for suggestions and feedback, in
-particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
+particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
 team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, 
 the Foundations group at Radboud university in Nijmegen, reporters of bugs
 and participants to the Coq-Club mailing list.
@@ -719,14 +719,14 @@ cleaned up the library of reals.
 
 The module system evolved significantly. Besides the resolution of
 some efficiency issues and a more flexible construction of module
-types, Élie Soubiran brought a new model of name equivalence, the
+types, Élie Soubiran brought a new model of name equivalence, the
 $\Delta$-equivalence, which respects as much as possible the names
 given by the users. He also designed with Pierre Letouzey a new
 convenient operator \verb!<+! for nesting functor application, what
 provides a light notation for inheriting the properties of cascading
 modules.
 
-The new tactic {\tt nsatz} is due to Loïc Pottier. It works by
+The new tactic {\tt nsatz} is due to Loïc Pottier. It works by
 computing Gr\"obner bases. Regarding the existing tactics, various
 improvements have been done by Matthieu Sozeau, Hugo Herbelin and
 Pierre Letouzey.
@@ -737,30 +737,30 @@ maintained and improved the extraction mechanism.  Bruno Barras and
 \'Elie Soubiran maintained the Coq checker, Julien Forest maintained
 the {\tt Function} mechanism for reasoning over recursively defined
 functions. Matthieu Sozeau, Hugo Herbelin and Jean-Marc Notin
-maintained {\tt coqdoc}. Frédéric Besson maintained the {\sc
+maintained {\tt coqdoc}. Frédéric Besson maintained the {\sc
   Micromega} plateform for deciding systems of inequalities. Pierre
 Courtieu maintained the support for the Proof General Emacs
-interface. Claude Marché maintained the plugin for calling external
+interface. Claude Marché maintained the plugin for calling external
 provers ({\tt dp}). Yves Bertot made some improvements to the
 libraries of lists and integers. Matthias Puech improved the search
 functions. Guillaume Melquiond usefully contributed here and
-there. Yann Régis-Gianas grounded the support for Unicode on a more
+there. Yann Régis-Gianas grounded the support for Unicode on a more
 standard and more robust basis.
 
 Though invisible from outside, Arnaud Spiwack improved the general
 process of management of existential variables. Pierre Letouzey and
-Stéphane Glondu improved the compilation scheme of the Coq archive.
+Stéphane Glondu improved the compilation scheme of the Coq archive.
 Vincent Gross provided support to {\CoqIDE}. Jean-Marc Notin provided
 support for benchmarking and archiving.
 
 Many users helped by reporting problems, providing patches, suggesting
 improvements or making useful comments, either on the bug tracker or
 on the Coq-club mailing list. This includes but not exhaustively
-Cédric Auger, Arthur Charguéraud, François Garillot, Georges Gonthier,
-Robin Green, Stéphane Lescuyer, Eelis van der Weegen,~...
+Cédric Auger, Arthur Charguéraud, François Garillot, Georges Gonthier,
+Robin Green, Stéphane Lescuyer, Eelis van der Weegen,~...
 
 Though not directly related to the implementation, special thanks are
-going to Yves Bertot, Pierre Castéran, Adam Chlipala, and Benjamin
+going to Yves Bertot, Pierre Castéran, Adam Chlipala, and Benjamin
 Pierce for the excellent teaching materials they provided.
 
 \begin{flushright}
@@ -913,7 +913,7 @@ interfaces has been designed by Pierre Letouzey.
 The general maintenance was done by Pierre Letouzey, Hugo Herbelin,
 Pierre Boutillier, Matthieu Sozeau and St\'ephane Glondu with also
 specific contributions from Guillaume Melquiond, Julien Narboux and
-Pierre-Marie Pédrot.
+Pierre-Marie Pédrot.
 
 Packaging tools were provided by Pierre Letouzey (Windows), Pierre
 Boutillier (MacOS), St\'ephane Glondu (Debian). Releasing, testing and
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index a133b059a..dc88a00ea 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -5,7 +5,7 @@
   \documentclass[11pt,a4paper]{book}
 %\fi
 
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{textcomp}
 \usepackage{times}
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index a2895cfcf..fdcc8a7b0 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1,7 +1,7 @@
 @String{jfp   = "Journal of Functional Programming"}
 @String{lncs  = "Lecture Notes in Computer Science"}
 @String{lnai  = "Lecture Notes in Artificial Intelligence"}
-@String{SV    = "{Sprin­ger-Verlag}"}
+@String{SV    = "{Sprin-ger-Verlag}"}
 
 @InProceedings{Aud91,
   author      = {Ph. Audebaud},
@@ -310,7 +310,7 @@ s},
   author      = {C. Cornes},
   month       = nov,
   school      = {{Universit\'e Paris 7}},
-  title       = {Conception d'un langage de haut niveau de représentation de preuves},
+  title       = {Conception d'un langage de haut niveau de représentation de preuves},
   type        = {Th\`ese de Doctorat},
   year        = {1997}
 }
@@ -436,7 +436,7 @@ s},
   editor      = {G. Huet and G. Plotkin},
   pages       = {59--79},
   publisher   = {Cambridge University Press},
-  title       = {Inductive sets and families in {Martin-Löf's}
+  title       = {Inductive sets and families in {Martin-Löf's}
  Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, 
   volume      = {14},
   year        = {1991}
@@ -456,7 +456,7 @@ s},
   author      = {J.-C. Filli\^atre},
   month       = sep,
   school      = {DEA d'Informatique, ENS Lyon},
-  title       = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}},
+  title       = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}},
   year        = {1994}
 }
 
@@ -470,7 +470,7 @@ s},
 }
 
 @Article{Filliatre03jfp,
-  author      = {J.-C. Filliâtre},
+  author      = {J.-C. Filliâtre},
   title       = {Verification of Non-Functional Programs 
                  using Interpretations in Type Theory},
   journal     = jfp,
@@ -488,7 +488,7 @@ s},
 @PhDThesis{Filliatre99,
   author      = {J.-C. Filli\^atre},
   title       = {Preuve de programmes imp\'eratifs en th\'eorie des types},
-  type        = {Thèse de Doctorat},
+  type        = {Thèse de Doctorat},
   school      = {Universit\'e Paris-Sud},
   year        = 1999,
   month       = {July},
@@ -607,7 +607,7 @@ s},
   author      = {D. Hirschkoff},
   month       = sep,
   school      = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
-  title       = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
+  title       = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
   year        = {1994}
 }
 
@@ -902,7 +902,7 @@ Intersection Types and Subtyping},
 }
 
 @MastersThesis{Mun94,
-  author      = {C. Muñoz},
+  author      = {C. Muñoz},
   month       = sep,
   school      = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
   title       = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
@@ -1012,7 +1012,7 @@ the Calculus of Inductive Constructions}},
   institution = {INRIA},
   month       = nov,
   number      = {1795},
-  title       = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}},
+  title       = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}},
   year        = {1992}
 }
 
@@ -1075,7 +1075,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}
 }
@@ -1177,7 +1177,7 @@ Decomposition}},
 @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
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index f0986fbf8..b66cbb436 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -9,8 +9,8 @@
 %\newcommand{\lnot}{not} % Hevea handles these symbols nicely
 %\newcommand{\lor}{or}
 %\newcommand{\land}{\&}
-%%% attention : -- dans un argument de \texttt est affiché comme un
-%%% seul - d'où l'utilisation de la macro suivante
+%%% Beware : in a \texttt, -- is displayed as a unique - hence
+%%% the following macro:
 \newcommand{\mm}{\symbol{45}\symbol{45}}