diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:00:10 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:14:41 +0100 |
commit | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (patch) | |
tree | 52eee33926e6791b4d2ac23c04f48404057899b4 /doc | |
parent | 56302f63809494946adf4e805bc61d55ed9d6f14 (diff) |
refman: switch all source files to utf8
Putting utf8 everywhere helps the maintainance of the online refman.
And anyway, this is the way to go. We should also chase and migrate
the few remaining iso-latin-1 files elsewhere in the sources.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/common/styles/html/coqremote/styles.hva | 2 | ||||
-rw-r--r-- | doc/common/styles/html/simple/styles.hva | 2 | ||||
-rw-r--r-- | doc/refman/AddRefMan-pre.tex | 10 | ||||
-rw-r--r-- | doc/refman/Coercion.tex | 2 | ||||
-rw-r--r-- | doc/refman/Extraction.tex | 2 | ||||
-rw-r--r-- | doc/refman/Micromega.tex | 2 | ||||
-rw-r--r-- | doc/refman/Nsatz.tex | 2 | ||||
-rw-r--r-- | doc/refman/Omega.tex | 4 | ||||
-rw-r--r-- | doc/refman/RefMan-cic.tex | 4 | ||||
-rw-r--r-- | doc/refman/RefMan-coi.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-ext.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-lib.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-pre.tex | 96 | ||||
-rw-r--r-- | doc/refman/Reference-Manual.tex | 2 | ||||
-rw-r--r-- | doc/refman/biblio.bib | 22 | ||||
-rw-r--r-- | doc/refman/coqdoc.tex | 4 |
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 = "{Springer-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}} |