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

Author: letouzey

CREDITS

@@ -17,7 +17,7 @@ All files of the "Coq proof assistant" in directories or sub-directories of
 
 are distributed under the terms of the GNU Lesser General Public License 
 Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010,
-The Coq development team, CNRS, INRIA and Universit� Paris Sud.
+The Coq development team, CNRS, INRIA and Université Paris Sud.
 
 Files from the directory doc are distributed as indicated in file doc/LICENCE.
 
@@ -29,9 +29,9 @@ plugins/cc
   developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
   University at Nijmegen, 2005-2008)
 plugins/correctness
-  developed by Jean-Christophe Filli�tre (LRI, 1999-2001)
+  developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
 plugins/dp
-  developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filli�tre
+  developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
   (LRI, 2005-2008)
 plugins/extraction
   developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
@@ -40,25 +40,25 @@ plugins/field
 plugins/firstorder 
   developed by Pierre Corbineau (LRI, 2003-2008)
 plugins/fourier
-  developed by Lo�c Pottier (INRIA-Lemme, 2001)
+  developed by Loïc Pottier (INRIA-Lemme, 2001)
 plugins/funind
   developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008),
   Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008) 
   and Yves Bertot (INRIA-Marelle, 2005-2006)
 plugins/omega
-  developed by Pierre Cr�gut (France Telecom R&D, 1996)
+  developed by Pierre Crégut (France Telecom R&D, 1996)
 plugins/nsatz
-  developed by Lo�c Pottier (INRIA-Marelle, 2009)
+  developed by Loïc Pottier (INRIA-Marelle, 2009)
 plugins/ring
   developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
   Loiseleur (LRI, 1997-1999)
 plugins/romega
-  developed by Pierre Cr�gut (France Telecom R&D, 2001-2004)
+  developed by Pierre Crégut (France Telecom R&D, 2001-2004)
 plugins/rtauto
   developed by Pierre Corbineau (LRI, 2005)
 plugins/setoid_ring
-  developed by Benjamin Gr�goire (INRIA-Everest, 2005-2006), 
-  Assia Mahboubi, Laurent Th�ry (INRIA-Marelle, 2006) 
+  developed by Benjamin Grégoire (INRIA-Everest, 2005-2006), 
+  Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006) 
   and Bruno Barras (INRIA LogiCal, 2005-2006),
 plugins/subtac
   developed by Matthieu Sozeau (LRI, 2005-2008)
@@ -67,18 +67,18 @@ plugins/xml
   as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
   part of the ProofWeb project (Radboud University at Nijmegen, 2008)
 plugins/micromega
-  developed by Fr�d�ric Besson (IRISA/INRIA, 2006-2008), with some 
+  developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some 
   extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and 
   interface to the csdp solver uses code from John Harrison (University
   of Cambridge, 1998)
 parsing/search.ml
   mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004)
 theories/ZArith
-  started by Pierre Cr�gut (France Telecom R&D, 1996)
+  started by Pierre Crégut (France Telecom R&D, 1996)
 theories/Strings
-  developed by Laurent Th�ry (INRIA-Lemme, 2003)
+  developed by Laurent Théry (INRIA-Lemme, 2003)
 theories/Numbers/Cyclic
-  developed by Benjamin Gr�goire (INRIA-Everest, 2007), Laurent Th�ry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008)
+  developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008)
 ide/utils
   some files come from Maxence Guesdon's Cameleon tool 
 
@@ -87,16 +87,16 @@ development influenced the design of Coq especially with
 
   C. Auger, Y. Bertot, F. Blanqui, J. Courant, P. Courtieu, J. Duprat,
   S. Glondu, J. Goubault, J.-P. Jouannaud, S. Lescuyer, A. Mahboubi,
-  C. March�, A. Miquel, B. Monate, L. Pottier, Y. R�gis-Gianas,
-  P.-Y. Strub, L. Th�ry, B. Werner
+  C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas,
+  P.-Y. Strub, L. Théry, B. Werner
 
 The development of Coq also significantly benefited from feedback,
 suggestions or short contributions from:
 
-  C. Alvarado, P. Cr�gut, J.-F. Monin (France Telecom R&D),
-  P. Cast�ran (University Bordeaux 1),
+  C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
+  P. Castéran (University Bordeaux 1),
   the Foundations Group (Radboud University, Nijmegen, The Netherlands),
-  Laboratoire J.-A. Dieudonn� (University of Nice-Sophia Antipolis),
+  Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis),
   F. Garillot, G. Gonthier (INRIA-MSR joint lab),
   INRIA-Gallium project, 
   the CS dept at Yale, the CIS dept at U. Penn, 
@@ -117,34 +117,34 @@ of the Coq Proof assistant during the indicated time:
   Olivier Desmettre (INRIA, 2001-2003)
   Gilles Dowek (INRIA, 1991-1994)
   Amy Felty (INRIA, 1993)
-  Jean-Christophe Filli�tre (ENS Lyon, 1994-1997, LRI, 1997-now)
-  Eduardo Gim�nez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
-  St�phane Glondu (INRIA-PPS, 2007-now)
-  Benjamin Gr�goire (INRIA, 2003-now)
+  Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-now)
+  Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
+  Stéphane Glondu (INRIA-PPS, 2007-now)
+  Benjamin Grégoire (INRIA, 2003-now)
   Hugo Herbelin (INRIA, 1996-now)
-  G�rard Huet (INRIA, 1985-1997)
+  Gérard Huet (INRIA, 1985-1997)
   Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now)
   Patrick Loiseleur (Paris Sud, 1997-1999)
   Evgeny Makarov (INRIA, 2007)
   Pascal Manoury (INRIA, 1993)
   Micaela Mayero (INRIA, 1997-2002)
-  Claude March� (INRIA 2003-2004 & LRI, 2004)
+  Claude Marché (INRIA 2003-2004 & LRI, 2004)
   Benjamin Monate (LRI, 2003)
-  C�sar Mu�oz (INRIA, 1994-1995)
+  César Muñoz (INRIA, 1994-1995)
   Chetan Murthy (INRIA, 1992-1994)
   Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now)
   Jean-Marc Notin (CNRS, 2006-now)
   Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
   Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, 
                             LRI, 1997-now)
-  Pierre-Marie P�drot (INRIA-PPS, 2011-now)
+  Pierre-Marie Pédrot (INRIA-PPS, 2011-now)
   Matthias Puech (INRIA-Bologna, 2008-now)
-  Yann R�gis-Gianas (INRIA-PPS, 2009-now)
-  Cl�ment Renard (INRIA, 2001-2004)
+  Yann Régis-Gianas (INRIA-PPS, 2009-now)
+  Clément Renard (INRIA, 2001-2004)
   Claudio Sacerdoti Coen (INRIA, 2004-2005)
-  Amokrane Sa�bi (INRIA, 1993-1998)
+  Amokrane Saïbi (INRIA, 1993-1998)
   Vincent Siles (INRIA, 2007)
-  �lie Soubiran (INRIA, 2007-now)
+  Élie Soubiran (INRIA, 2007-now)
   Matthieu Sozeau (INRIA, 2005-now)
   Arnaud Spiwack (INRIA, 2006-now)
   Enrico Tassi (INRIA, 2011-now)
@@ -156,9 +156,9 @@ INRIA refers to:
 CNRS refers to:
   Centre National de la Recherche Scientifique
 LRI refers to: Laboratoire de Recherche en Informatique, UMR 8623
-  CNRS and Universit� Paris-Sud
+  CNRS and Université Paris-Sud
 ENS Lyon refers to:
-  Ecole Normale Sup�rieure de Lyon
-PPS refers to: Laboratoire Preuve, Programmation, Syst�me, UMR 7126,
-  CNRS and Universit� Paris 7
+  Ecole Normale Supérieure de Lyon
+PPS refers to: Laboratoire Preuve, Programmation, Système, UMR 7126,
+  CNRS and Université Paris 7
 ****************************************************************************

TODO

@@ -25,29 +25,29 @@ Theories:
 
 Doc:
 
-- Mettre � jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
+- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
 - Documenter le filtrage sur les types inductifs avec let-ins (dont la
   compatibilite V6)
 
-- Ajouter let dans les r�gles du CIC
+- Ajouter let dans les règles du CIC
   -> FAIT, mais reste a documenter le let dans les inductifs
   et les champs manifestes dans les Record   
 - revoir le chapitre sur les tactiques utilisateur 
-- faut-il mieux sp�cifier la s�mantique de Simpl (??)
+- faut-il mieux spécifier la sémantique de Simpl (??)
 
-- Pr�ciser la clarification syntaxique de IntroPattern
+- Préciser la clarification syntaxique de IntroPattern
 - preciser que Goal vient en dernier dans une clause pattern list et
   qu'il doit apparaitre si il y a un "in"
 
 - Omega Time debranche mais Omega System et Omega Action remarchent ?
 - Ajout "Replace in" (mais TODO)
-- Syntaxe Conditional tac Rewrite marche, � documenter
+- Syntaxe Conditional tac Rewrite marche, à documenter
 - Documenter Dependent Rewrite et CutRewrite ?
 - Ajouter les motifs sous-termes de ltac
 
 - ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.)
-- mettre � jour la doc de induction (arguments multiples) (Pierre C.)
-- mettre � jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
---> mettre � jour le CHANGES (vers la ligne 72)
+- mettre à jour la doc de induction (arguments multiples) (Pierre C.)
+- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
+--> mettre à jour le CHANGES (vers la ligne 72)
 
 

dev/TODO

@@ -3,16 +3,16 @@
      - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml
 
  o arguments implicites
-     - les calculer une fois pour toutes � la d�claration (dans Declare)
+     - les calculer une fois pour toutes à la déclaration (dans Declare)
        et stocker cette information dans le in_variable, in_constant, etc.
 
- o Environnements compil�s (type Environ.compiled_env)
-     - pas de timestamp mais plut�t un checksum avec Digest (mais comment ?)
+ o Environnements compilés (type Environ.compiled_env)
+     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)
 
- o Efficacit�
-     - utiliser DOPL plut�t que DOPN (sauf pour Case)
+ o Efficacité
+     - utiliser DOPL plutôt que DOPN (sauf pour Case)
      - batch mode => pas de undo, ni de reset
-     - conversion : d�plier la constante la plus r�cente
+     - conversion : déplier la constante la plus récente
      - un cache pour type_of_const, type_of_inductive, type_of_constructor,
        lookup_mind_specif
 

dev/doc/changes.txt

@@ -615,14 +615,14 @@ Changements d'organisation / modules :
   Std, More_util		-> lib/util.ml
 
   Names				-> kernel/names.ml et kernel/sign.ml
-    (les parties noms et signatures ont �t� s�par�es)
+    (les parties noms et signatures ont été séparées)
 
-  Avm,Mavm,Fmavm,Mhm  ->  utiliser plut�t Map (et freeze alors gratuit)
+  Avm,Mavm,Fmavm,Mhm  ->  utiliser plutôt Map (et freeze alors gratuit)
   Mhb                 ->  Bij
 
-  Generic est int�gr� � Term (et un petit peu � Closure)
+  Generic est intégré à Term (et un petit peu à Closure)
 
-Changements dans les types de donn�es :
+Changements dans les types de données :
 ---------------------------------------
   dans Generic: free_rels : constr -> int Listset.t
                   devient : constr -> Intset.t
@@ -642,7 +642,7 @@ ATTENTION:
 
 		try . .. with UserError _ -> ...
 
-  mais �crire � la place
+  mais écrire à la place
 
                 try ... with e when Logic.catchable_exception e -> ...
 
@@ -774,40 +774,40 @@ Changements dans les inductifs
 Nouveaux types "constructor" et "inductive" dans Term
 La plupart des fonctions de typage des inductives prennent maintenant
 un inductive au lieu d'un oonstr comme argument. Les seules fonctions
-� traduire un constr en inductive sont les find_rectype and co.
+à traduire un constr en inductive sont les find_rectype and co.
 
 Changements dans les grammaires
 -------------------------------
 
  . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex
 
  . attention : LIDENT -> IDENT  (les identificateurs n'ont pas de
-                                 casse particuli�re dans Coq)
+                                 casse particulière dans Coq)
 
- . Le mot "command" est remplac� par "constr" dans les noms de
+ . Le mot "command" est remplacé par "constr" dans les noms de
  fichiers, noms de modules et non-terminaux relatifs au parsing des
  termes; aussi les changements suivants "COMMAND"/"CONSTR" dans
  g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml*
 
  . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n
    passent en minuscule Identifier, Constr, ...
 
- . Plusieurs parsers ont chang� de format (ex: sortarg)
+ . Plusieurs parsers ont changé de format (ex: sortarg)
 
 Changements dans le pretty-printing
 -----------------------------------
 
- . D�couplage de la traduction de constr -> rawconstr (dans detyping)
+ . Découplage de la traduction de constr -> rawconstr (dans detyping)
     et de rawconstr -> ast (dans termast)
- . D�placement des options d'affichage de printer vers termast
- . D�placement des r�aiguillage d'univers du pp de printer vers esyntax
+ . Déplacement des options d'affichage de printer vers termast
+ . Déplacement des réaiguillage d'univers du pp de printer vers esyntax
 
 
 Changements divers
 ------------------
 
  . il n'y a plus de script coqtop => coqtop et coqtop.byte sont
-   directement le r�sultat du link du code
+   directement le résultat du link du code
    => debuggage et profiling directs
 
  . il n'y a plus d'installation locale dans bin/$ARCH

dev/doc/extensions.txt

@@ -1,19 +1,19 @@
-Comment ajouter une nouvelle entr�e primitive pour les TACTIC EXTEND ?
+Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ?
 ======================================================================
 
-Exemple de l'ajout de l'entr�e "clause":
+Exemple de l'ajout de l'entrée "clause":
 
 - ajouter un type ClauseArgType dans interp/genarg.ml{,i}, avec les
   wit_, rawwit_, et globwit_ correspondants
 
-- ajouter partout o� Genarg.argument_type est filtr� le cas traitant de
+- ajouter partout où Genarg.argument_type est filtré le cas traitant de
   ce nouveau ClauseArgType
 
-- utiliser le rawwit_clause pour d�finir une entr�e clause du bon
+- utiliser le rawwit_clause pour définir une entrée clause du bon
   type et du bon nom dans le module Tactic de pcoq.ml4
 
-- il faut aussi exporter la r�gle hors de g_tactic.ml4. Pour cela, il
+- il faut aussi exporter la règle hors de g_tactic.ml4. Pour cela, il
   faut rejouter clause dans le GLOBAL du GEXTEND
 
-- seulement apr�s, le nom clause sera accessible dans les TACTIC EXTEND !
+- seulement après, le nom clause sera accessible dans les TACTIC EXTEND !
 

dev/doc/naming-conventions.tex

@@ -1,6 +1,6 @@
 \documentclass[a4paper]{article}
 \usepackage{fullpage}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{amsfonts}
 
@@ -299,7 +299,7 @@ \subsection{Specific conventions}
     (for \texttt{Z}, \texttt{Q} and \texttt{R}), \texttt{eq\_mul\_0} (for
     \texttt{NZ}).
 
-  Remark: The French school says ``integrité''.
+  Remark: The French school says ``integrité''.
 
 \itemrule{Nilpotency of binary operator {\op} wrt to its absorbing element
 zero in D}{Dop\_nilpotent} {forall x, op x x = zero}