[Sphinx] Move credits to new infrastructure

1 files changed, 1351 insertions, 0 deletions

diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
new file mode 100644
index 000000000..05775bfbe
--- /dev/null
+++ b/doc/sphinx/credits.rst
@@ -0,0 +1,1351 @@
+%BEGIN LATEX
+\setheaders{Credits}
+%END LATEX
+\chapter*{Credits}
+%HEVEA\cutname{credits.html}
+%\addcontentsline{toc}{section}{Credits}
+
+\Coq{}~ is a proof assistant for higher-order logic, allowing the
+development of computer programs consistent with their formal
+specification.  It is the result of about ten years of research of the
+Coq project.  We shall briefly survey here three main aspects: the
+\emph{logical language} in which we write our axiomatizations and
+specifications, the \emph{proof assistant} which allows the development
+of verified mathematical proofs, and the \emph{program extractor} which
+synthesizes computer programs obeying their formal specifications,
+written as logical assertions in the language.
+
+The logical language used by {\Coq} is a variety of type theory,
+called the \emph{Calculus of Inductive Constructions}. Without going
+back to Leibniz and Boole, we can date the creation of what is now
+called mathematical logic to the work of Frege and Peano at the turn
+of the century. The discovery of antinomies in the free use of
+predicates or comprehension principles prompted Russell to restrict
+predicate calculus with a stratification of \emph{types}. This effort
+culminated with \emph{Principia Mathematica}, the first systematic
+attempt at a formal foundation of mathematics.  A simplification of
+this system along the lines of simply typed $\lambda$-calculus
+occurred with Church's \emph{Simple Theory of Types}.  The
+$\lambda$-calculus notation, originally used for expressing
+functionality, could also be used as an encoding of natural deduction
+proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the
+\emph{Automath} project, the first full-scale attempt to develop and
+mechanically verify mathematical proofs. This effort culminated with
+Jutting's verification of Landau's \emph{Grundlagen} in the 1970's.
+Exploiting this Curry-Howard isomorphism, notable achievements in
+proof theory saw the emergence of two type-theoretic frameworks; the
+first one, Martin-L\"of's \emph{Intuitionistic Theory of Types},
+attempts a new foundation of mathematics on constructive principles.
+The second one, Girard's polymorphic $\lambda$-calculus $F_\omega$, is
+a very strong functional system in which we may represent higher-order
+logic proof structures.  Combining both systems in a higher-order
+extension of the Automath languages, T. Coquand presented in 1985 the
+first version of the \emph{Calculus of Constructions}, CoC. This strong
+logical system allowed powerful axiomatizations, but direct inductive
+definitions were not possible, and inductive notions had to be defined
+indirectly through functional encodings, which introduced
+inefficiencies and awkwardness. The formalism was extended in 1989 by
+T. Coquand and C. Paulin with primitive inductive definitions, leading
+to the current \emph{Calculus of Inductive Constructions}.  This
+extended formalism is not rigorously defined here. Rather, numerous
+concrete examples are discussed. We refer the interested reader to
+relevant research papers for more information about the formalism, its
+meta-theoretic properties, and semantics. However, it should not be
+necessary to understand this theoretical material in order to write
+specifications. It is possible to understand the Calculus of Inductive
+Constructions at a higher level, as a mixture of predicate calculus,
+inductive predicate definitions presented as typed PROLOG, and
+recursive function definitions close to the language ML.
+
+Automated theorem-proving was pioneered in the 1960's by Davis and
+Putnam in propositional calculus.  A complete mechanization (in the
+sense of a semi-decision procedure) of classical first-order logic was
+proposed in 1965 by J.A. Robinson, with a single uniform inference
+rule called \emph{resolution}. Resolution relies on solving equations
+in free algebras (i.e. term structures), using the \emph{unification
+  algorithm}. Many refinements of resolution were studied in the
+1970's, but few convincing implementations were realized, except of
+course that PROLOG is in some sense issued from this effort.  A less
+ambitious approach to proof development is computer-aided
+proof-checking.  The most notable proof-checkers developed in the
+1970's were LCF, designed by R. Milner and his colleagues at U.
+Edinburgh, specialized in proving properties about denotational
+semantics recursion equations, and the Boyer and Moore theorem-prover,
+an automation of primitive recursion over inductive data types. While
+the Boyer-Moore theorem-prover attempted to synthesize proofs by a
+combination of automated methods, LCF constructed its proofs through
+the programming of \emph{tactics}, written in a high-level functional
+meta-language, ML.
+
+The salient feature which clearly distinguishes our proof assistant
+from say LCF or Boyer and Moore's, is its possibility to extract
+programs from the constructive contents of proofs. This computational
+interpretation of proof objects, in the tradition of Bishop's
+constructive mathematics, is based on a realizability interpretation,
+in the sense of Kleene, due to C.  Paulin. The user must just mark his
+intention by separating in the logical statements the assertions
+stating the existence of a computational object from the logical
+assertions which specify its properties, but which may be considered
+as just comments in the corresponding program. Given this information,
+the system automatically extracts a functional term from a consistency
+proof of its specifications.  This functional term may be in turn
+compiled into an actual computer program.  This methodology of
+extracting programs from proofs is a revolutionary paradigm for
+software engineering.  Program synthesis has long been a theme of
+research in artificial intelligence, pioneered by R. Waldinger. The
+Tablog system of Z. Manna and R. Waldinger allows the deductive
+synthesis of functional programs from proofs in tableau form of their
+specifications, written in a variety of first-order logic. Development
+of a systematic \emph{programming logic}, based on extensions of
+Martin-L\"of's type theory, was undertaken at Cornell U. by the Nuprl
+team, headed by R. Constable.  The first actual program extractor, PX,
+was designed and implemented around 1985 by S. Hayashi from Kyoto
+University.  It allows the extraction of a LISP program from a proof
+in a logical system inspired by the logical formalisms of S. Feferman.
+Interest in this methodology is growing in the theoretical computer
+science community. We can foresee the day when actual computer systems
+used in applications will contain certified modules, automatically
+generated from a consistency proof of their formal specifications. We
+are however still far from being able to use this methodology in a
+smooth interaction with the standard tools from software engineering,
+i.e. compilers, linkers, run-time systems taking advantage of special
+hardware, debuggers, and the like. We hope that {\Coq} can be of use
+to researchers interested in experimenting with this new methodology.
+
+A first implementation of CoC was started in 1984 by G. Huet and T.
+Coquand.  Its implementation language was CAML, a functional
+programming language from the ML family designed at INRIA in
+Rocquencourt. The core of this system was a proof-checker for CoC seen
+as a typed $\lambda$-calculus, called the \emph{Constructive Engine}.
+This engine was operated through a high-level notation permitting the
+declaration of axioms and parameters, the definition of mathematical
+types and objects, and the explicit construction of proof objects
+encoded as $\lambda$-terms. A section mechanism, designed and
+implemented by G. Dowek, allowed hierarchical developments of
+mathematical theories. This high-level language was called the
+\emph{Mathematical Vernacular}.  Furthermore, an interactive
+\emph{Theorem Prover} permitted the incremental construction of proof
+trees in a top-down manner, subgoaling recursively and backtracking
+from dead-alleys. The theorem prover executed tactics written in CAML,
+in the LCF fashion.  A basic set of tactics was predefined, which the
+user could extend by his own specific tactics. This system (Version
+4.10) was released in 1989.  Then, the system was extended to deal
+with the new calculus with inductive types by C. Paulin, with
+corresponding new tactics for proofs by induction.  A new standard set
+of tactics was streamlined, and the vernacular extended for tactics
+execution. A package to compile programs extracted from proofs to
+actual computer programs in CAML or some other functional language was
+designed and implemented by B. Werner.  A new user-interface, relying
+on a CAML-X interface by D. de Rauglaudre, was designed and
+implemented by A. Felty. It allowed operation of the theorem-prover
+through the manipulation of windows, menus, mouse-sensitive buttons,
+and other widgets. This system (Version 5.6) was released in 1991.
+
+\Coq{} was ported to the new implementation Caml-light of X. Leroy and
+D.  Doligez by D. de Rauglaudre (Version 5.7) in 1992.  A new version
+of \Coq{} was then coordinated by C. Murthy, with new tools designed
+by C.  Parent to prove properties of ML programs (this methodology is
+dual to program extraction) and a new user-interaction loop.  This
+system (Version 5.8) was released in May 1993.  A Centaur interface
+\textsc{CTCoq} was then developed by Y. Bertot from the Croap project
+from INRIA-Sophia-Antipolis.
+
+In parallel, G. Dowek and H. Herbelin developed a new proof engine,
+allowing the general manipulation of existential variables
+consistently with dependent types in an experimental version of \Coq{}
+(V5.9).
+
+The version V5.10 of \Coq{} is based on a generic system for
+manipulating terms with binding operators due to Chet Murthy. A new
+proof engine allows the parallel development of partial proofs for
+independent subgoals.  The structure of these proof trees is a mixed
+representation of derivation trees for the Calculus of Inductive
+Constructions with abstract syntax trees for the tactics scripts,
+allowing the navigation in a proof at various levels of details. The
+proof engine allows generic environment items managed in an
+object-oriented way.  This new architecture, due to C. Murthy,
+supports several new facilities which make the system easier to extend
+and to scale up:
+
+\begin{itemize}
+\item User-programmable tactics are allowed
+\item It is possible to separately verify development modules, and to
+  load their compiled images without verifying them again - a quick
+  relocation process allows their fast loading
+\item A generic parsing scheme allows user-definable notations, with a
+  symmetric table-driven pretty-printer
+\item Syntactic definitions allow convenient abbreviations
+\item A limited facility of meta-variables allows the automatic
+  synthesis of certain type expressions, allowing generic notations
+  for e.g. equality, pairing, and existential quantification.
+\end{itemize}
+
+In the Fall of 1994, C. Paulin-Mohring replaced the structure of
+inductively defined types and families by a new structure, allowing
+the mutually recursive definitions. P. Manoury implemented a
+translation of recursive definitions into the primitive recursive
+style imposed by the internal recursion operators, in the style of the
+ProPre system. C. Mu{\~n}oz implemented a decision procedure for
+intuitionistic propositional logic, based on results of R. Dyckhoff.
+J.C. Filli{\^a}tre implemented a decision procedure for first-order
+logic without contraction, based on results of J. Ketonen and R.
+Weyhrauch. Finally C. Murthy implemented a library of inversion
+tactics, relieving the user from tedious definitions of ``inversion
+predicates''.
+
+\begin{flushright}
+Rocquencourt, Feb. 1st 1995\\
+Gérard Huet
+\end{flushright}
+
+\section*{Credits: addendum for version 6.1}
+%\addcontentsline{toc}{section}{Credits: addendum for version V6.1}
+
+The present version 6.1 of \Coq{} is based on the V5.10 architecture. It
+was ported to the new language {\ocaml} by Bruno Barras. The
+underlying framework has slightly changed and allows more conversions
+between sorts. 
+
+The new version provides powerful tools for easier developments. 
+
+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
+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
+do not need to be explicitly written. 
+
+Yann Coscoy designed a command which explains a proof term using
+natural language. Pierre Cr{\'e}gut built a new tactic which solves
+problems in quantifier-free Presburger Arithmetic. Both
+functionalities have been integrated to the \Coq{} system by Hugo
+Herbelin.
+
+Samuel Boutin designed a tactic for simplification of commutative
+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
+and Bruno Barras.
+
+\begin{flushright}
+Lyon, Nov. 18th 1996\\
+Christine Paulin
+\end{flushright}
+
+\section*{Credits: addendum for version 6.2}
+%\addcontentsline{toc}{section}{Credits: addendum for version V6.2}
+
+In version 6.2 of \Coq{}, the parsing is done using camlp4, a
+preprocessor and pretty-printer for CAML designed by Daniel de
+Rauglaudre at INRIA.  Daniel de Rauglaudre made the first adaptation
+of \Coq{} for camlp4, this work was continued by Bruno Barras who also
+changed the structure of \Coq{} abstract syntax trees and the primitives
+to manipulate them. The result of
+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
+tactic libraries, giving uniform names 
+to Caml functions corresponding to \Coq{} tactic names. 
+
+Bruno Barras wrote new more efficient reductions functions.
+
+Hugo Herbelin introduced more uniform notations in the \Coq{}
+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
+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
+generalizes the previous tactic implemented by Samuel Boutin.
+Jean-Christophe Filli\^atre introduced a tactic for refining a goal,
+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.
+
+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.
+
+\begin{flushright}
+Orsay, May 4th 1998\\
+Christine Paulin
+\end{flushright}
+
+\section*{Credits: addendum for version 6.3}
+The main changes in version V6.3 was the introduction of a few new tactics
+and the extension of the guard condition for fixpoint definitions.
+
+
+B. Barras extended the unification algorithm to complete partial terms
+and solved various tricky bugs related to universes.\\
+D. Delahaye developed the \texttt{AutoRewrite} tactic. He also designed the new
+behavior of \texttt{Intro} and provided the tacticals \texttt{First} and
+\texttt{Solve}.\\
+J.-C. Filli\^atre developed the \texttt{Correctness} tactic.\\
+E. Gim\'enez extended the guard condition in fixpoints.\\
+H. Herbelin designed the new syntax for definitions and extended the
+\texttt{Induction} tactic.\\
+P. Loiseleur developed the \texttt{Quote} tactic and 
+the new design of the \texttt{Auto}
+tactic, he also introduced the index of
+errors in the documentation.\\
+C. Paulin wrote the \texttt{Focus} command and introduced 
+the reduction functions in definitions, this last feature 
+was proposed by J.-F. Monin from CNET Lannion. 
+
+\begin{flushright}
+Orsay, Dec. 1999\\
+Christine Paulin
+\end{flushright}
+
+%\newpage
+
+\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
+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
+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
+of modules and also to get closer to a certified kernel.
+
+Hugo Herbelin introduced a new structure of terms with local
+definitions. He introduced ``qualified'' names, wrote a new
+pattern-matching compilation algorithm and designed a more compact
+algorithm for checking the logical consistency of universes. He
+contributed to the simplification of {\Coq} internal structures and the
+optimisation of the system. He added basic tactics for forward
+reasoning and coercions in patterns.
+
+David Delahaye introduced a new language for tactics. General tactics
+using pattern-matching on goals and context can directly be written
+from the {\Coq} toplevel. He also provided primitives for the design
+of user-defined tactics in \textsc{Caml}.
+
+Micaela Mayero contributed the library on real numbers.
+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
+extraction procedure from \Coq{} terms to \textsc{Caml} or
+\textsc{Haskell} programs. This new 
+extraction procedure, unlike the one implemented in previous version
+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
+tool for {\Coq} libraries usable from version 7.2.
+
+Bruno Barras improved the reduction algorithms efficiency and
+the confidence level in the correctness of {\Coq} critical type-checking
+algorithm.
+
+Yves Bertot designed  the \texttt{SearchPattern} and
+\texttt{SearchRewrite} tools and the support for the \textsc{pcoq} interface 
+(\url{http://www-sop.inria.fr/lemme/pcoq/}).
+
+Micaela Mayero and David Delahaye introduced {\tt Field}, a decision tactic for commutative fields.
+
+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.
+
+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}
+modules to be used in the Hypertextual Electronic Library of
+Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}).
+
+A library for efficient representation of finite maps using binary trees
+contributed by Jean Goubault was integrated in the basic theories.
+
+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.
+
+\bigskip
+
+The development was coordinated by C. Paulin.
+
+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.
+
+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
+\end{flushright}
+
+\section*{Credits: version 8.0}
+
+{\Coq} version 8 is a major revision of the {\Coq} proof assistant.
+First, the underlying logic is slightly different. The so-called {\em
+impredicativity} of the sort {\tt Set} has been dropped. The main
+reason is that it is inconsistent with the principle of description
+which is quite a useful principle for formalizing %classical
+mathematics within classical logic. Moreover, even in an constructive
+setting, the impredicativity of {\tt Set} does not add so much in
+practice and is even subject of criticism from a large part of the
+intuitionistic mathematician community. Nevertheless, the
+impredicativity of {\tt Set} remains optional for users interested in
+investigating mathematical developments which rely on it.
+
+Secondly, the concrete syntax of terms has been completely
+revised. The main motivations were
+
+\begin{itemize}
+\item a more uniform, purified style: all constructions are now lowercase, 
+  with a functional programming perfume (e.g. abstraction is now
+  written {\tt fun}), and more directly accessible to the novice
+  (e.g. dependent product is now written {\tt forall} and allows
+  omission of types). Also, parentheses and are no longer mandatory
+  for function application.
+\item extensibility: some standard notations (e.g. ``<'' and ``>'') were
+  incompatible with the previous syntax. Now all standard arithmetic
+  notations (=, +, *, /, <, <=, ... and more) are directly part of the
+  syntax.
+\end{itemize}
+
+Together with the revision of the concrete syntax, a new mechanism of
+{\em interpretation scopes} permits to reuse the same symbols
+(typically +, -, *, /, <, <=) in various mathematical theories without
+any ambiguities for {\Coq}, leading to a largely improved readability of
+{\Coq} scripts. New commands to easily add new symbols are also
+provided.
+
+Coming with the new syntax of terms, a slight reform of the tactic
+language and of the language of commands has been carried out. The
+purpose here is a better uniformity making the tactics and commands
+easier to use and to remember.
+
+Thirdly, a restructuration and uniformisation of the standard library
+of {\Coq} has been performed. There is now just one Leibniz' equality
+usable for all the different kinds of {\Coq} objects. Also, the set of
+real numbers now lies at the same level as the sets of natural and
+integer numbers. Finally, the names of the standard properties of
+numbers now follow a standard pattern and the symbolic
+notations for the standard definitions as well.
+
+The fourth point is the release of \CoqIDE{}, a new graphical
+gtk2-based interface fully integrated to {\Coq}. Close in style from
+the Proof General Emacs interface, it is faster and its integration
+with {\Coq} makes interactive developments more friendly. All
+mathematical Unicode symbols are usable within \CoqIDE{}.
+
+Finally, the module system of {\Coq} completes the picture of {\Coq}
+version 8.0. Though released with an experimental status in the previous
+version 7.4, it should be considered as a salient feature of the new
+version.
+
+Besides, {\Coq} comes with its load of novelties and improvements: new
+or improved tactics (including a new tactic for solving first-order
+statements), new management commands, extended libraries.
+
+\bigskip
+
+Bruno Barras and Hugo Herbelin have been the main contributors of the 
+reflexion and the implementation of the new syntax. The smart
+automatic translator from old to new syntax released with {\Coq} is also
+their work with contributions by Olivier Desmettre.
+
+Hugo Herbelin is the main designer and implementor of the notion of
+interpretation scopes and of the commands for easily adding new notations.
+
+Hugo Herbelin is the main implementor of the restructuration of the
+standard library.
+
+Pierre Corbineau is the main designer and implementor of the new
+tactic for solving first-order statements in presence of inductive
+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.
+
+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 other
+contributors from Sophia-Antipolis and Nijmegen participated to the
+extension of the library.
+
+Julien Narboux built a NSIS-based automatic {\Coq} installation tool for
+the Windows platform.
+
+Hugo Herbelin and Christine Paulin coordinated the development which
+was under the responsability of Christine Paulin.
+
+\begin{flushright}
+Palaiseau \& Orsay, Apr. 2004\\
+Hugo Herbelin \& Christine Paulin\\
+(updated Apr. 2006)
+\end{flushright}
+
+\section*{Credits: version 8.1}
+
+{\Coq} version 8.1 adds various new functionalities.
+
+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
+machine.  Convertibility is performed by comparing the normal
+forms. This alternative algorithm is specifically interesting for
+proofs by reflection. More generally, it is convenient in case of
+intensive computations.
+
+Christine Paulin implemented an extension of inductive types allowing
+recursively non uniform parameters. Hugo Herbelin implemented
+sort-polymorphism for inductive types (now called template polymorphism).
+
+Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary
+compatible equivalence relations. He also generalized rewriting to
+arbitrary transition systems.
+
+Claudio Sacerdoti Coen added new features to the module system. 
+
+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
+simplification algorithm on fields.
+
+Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
+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
+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.
+
+Matthieu Sozeau developed \textsc{Russell}, an experimental language
+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
+integrated to the {\Coq} standard library. Pierre Letouzey developed a
+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..
+
+Pierre Corbineau extended his tactic for solving first-order
+statements. He wrote a reflection-based intuitionistic tautology
+solver.
+
+Pierre Courtieu, Julien Forest and Yves Bertot added extra support to
+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
+types and suggested improvements to the libraries.
+
+Pierre Corbineau implemented a declarative mathematical proof
+language, usable in combination with the tactic-based style of proof.
+
+Finally, many users suggested improvements of the system through the
+Coq-Club mailing list and bug-tracker systems, especially user groups
+from INRIA Rocquencourt, Radboud University, University of
+Pennsylvania and Yale University.
+
+\enlargethispage{\baselineskip}
+\begin{flushright}
+Palaiseau, July 2006\\
+Hugo Herbelin
+\end{flushright}
+
+\section*{Credits: version 8.2}
+
+{\Coq} version 8.2 adds new features, new libraries and 
+improves on many various aspects.
+
+Regarding the language of Coq, the main novelty is the introduction by
+Matthieu Sozeau of a package of commands providing Haskell-style
+type classes. Type classes, that come with a few convenient features
+such as type-based resolution of implicit arguments, plays a new role
+of landmark in the architecture of Coq with respect to automatization.
+For instance, thanks to type classes support, Matthieu Sozeau could
+implement a new resolution-based version of the tactics dedicated to
+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
+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,
+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
+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
+``certificate'' for the Positivstellensatz and this covers the case of
+Fourier-Motzkin (for linear systems in $\mathbb{Q}$ and $\mathbb{R}$),
+Fourier-Motzkin with cutting planes (for linear systems in
+$\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
+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
+version 8.1 to use 31-bits machine arithmetics for efficiently
+computing with the library of integers he developed.
+
+Beside the libraries, various improvements contributed to provide a
+more comfortable end-user language and more expressive tactic
+language. Hugo Herbelin and Matthieu Sozeau improved the
+pattern-matching compilation algorithm (detection of impossible
+clauses in pattern-matching, automatic inference of the return
+type). Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau contributed
+various new convenient syntactic constructs and new tactics or tactic
+features: more inference of redundant information, better unification,
+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
+an ``include'' command) and making it more flexible and more
+general. He and Pierre Letouzey improved the support for modules in
+the extraction mechanism.
+
+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 of 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
+of {\tt injection}.
+
+Bruno Barras implemented the {\tt coqchk} tool: this is a stand-alone
+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
+Julien Forest acted as maintainers of features they implemented in
+previous versions of Coq.
+
+Julien Narboux contributed to {\CoqIDE}.
+Nicolas Tabareau made the adaptation of the interface of the old
+``setoid rewrite'' tactic to the new version. Lionel Mamane worked on
+the interaction between Coq and its external interfaces. With Samuel
+Mimram, he also helped making Coq compatible with recent software
+tools.  Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to
+improve 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
+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.
+
+\begin{flushright}
+Palaiseau, June 2008\\
+Hugo Herbelin\\
+\end{flushright}
+
+\section*{Credits: version 8.3}
+
+{\Coq} version 8.3 is before all a transition version with refinements
+or extensions of the existing features and libraries and a new tactic
+{\tt nsatz} based on Hilbert's Nullstellensatz for deciding systems of
+equations over rings.
+
+With respect to libraries, the main evolutions are due to Pierre
+Letouzey with a rewriting of the library of finite sets {\tt FSets}
+and a new round of evolutions in the modular development of arithmetic
+(library {\tt Numbers}). The reason for making {\tt FSets} evolve is
+that the computational and logical contents were quite intertwined in
+the original implementation, leading in some cases to longer
+computations than expected and this problem is solved in the new {\tt
+  MSets} implementation. As for the modular arithmetic library, it was
+only dealing with the basic arithmetic operators in the former version
+and its current extension adds the standard theory of the division,
+min and max functions, all made available for free to any
+implementation of $\mathbb{N}$, $\mathbb{Z}$ or
+$\mathbb{Z}/n\mathbb{Z}$. 
+
+The main other evolutions of the library are due to Hugo Herbelin who
+made a revision of the sorting library (including a certified
+merge-sort) and to Guillaume Melquiond who slightly revised and
+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
+$\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, that
+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
+computing Gr\"obner bases. Regarding the existing tactics, various
+improvements have been done by Matthieu Sozeau, Hugo Herbelin and
+Pierre Letouzey.
+
+Matthieu Sozeau extended and refined the type classes and {\tt
+  Program} features (the {\sc Russell} language). Pierre Letouzey
+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
+  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
+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
+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.
+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,~...
+
+Though not directly related to the implementation, special thanks are
+going to Yves Bertot, Pierre Castéran, Adam Chlipala, and Benjamin
+Pierce for the excellent teaching materials they provided.
+
+\begin{flushright}
+Paris, April 2010\\
+Hugo Herbelin\\
+\end{flushright}
+
+\section*{Credits: version 8.4}
+
+{\Coq} version 8.4 contains the result of three long-term projects: a
+new modular library of arithmetic by Pierre Letouzey, a new proof
+engine by Arnaud Spiwack and a new communication protocol for {\CoqIDE}
+by Vincent Gross.
+
+The new modular library of arithmetic extends, generalizes and
+unifies the existing libraries on Peano arithmetic (types {\tt nat},
+{\tt N} and {\tt BigN}), positive arithmetic (type {\tt positive}),
+integer arithmetic ({\tt Z} and {\tt BigZ}) and machine word
+arithmetic (type {\tt Int31}). It provides with unified notations
+(e.g. systematic use of {\tt add} and {\tt mul} for denoting the
+addition and multiplication operators), systematic and generic
+development of operators and properties of these operators for all the
+types mentioned above, including gcd, pcm, power, square root, base 2
+logarithm, division, modulo, bitwise operations, logical shifts,
+comparisons, iterators, ...
+
+The most visible feature of the new proof engine is the support for
+structured scripts (bullets and proof brackets) but, even if yet not
+user-available, the new engine also provides the basis for refining
+existential variables using tactics, for applying tactics to several
+goals simultaneously, for reordering goals, all features which are
+planned for the next release. The new proof engine forced to
+reimplement {\tt info} and {\tt Show Script} differently, what was
+done by Pierre Letouzey.
+
+Before version 8.4, {\CoqIDE} was linked to {\Coq} with the graphical
+interface living in a separate thread. From version 8.4, {\CoqIDE} is a
+separate process communicating with {\Coq} through a textual
+channel. This allows for a more robust interfacing, the ability to
+interrupt {\Coq} without interrupting the interface, and the ability to
+manage several sessions in parallel. Relying on the infrastructure
+work made by Vincent Gross, Pierre Letouzey, Pierre Boutillier and
+Pierre-Marie P\'edrot contributed many various refinements of {\CoqIDE}.
+
+{\Coq} 8.4 also comes with a bunch of many various smaller-scale changes
+and improvements regarding the different components of the system.
+
+The underlying logic has been extended with $\eta$-conversion thanks
+to Hugo Herbelin, St\'ephane Glondu and Benjamin Gr\'egoire. The
+addition of $\eta$-conversion is justified by the confidence that the
+formulation of the Calculus of Inductive Constructions based on typed
+equality (such as the one considered in Lee and Werner to build a
+set-theoretic model of CIC~\cite{LeeWerner11}) is applicable to the
+concrete implementation of {\Coq}.
+
+The underlying logic benefited also from a refinement of the guard
+condition for fixpoints by Pierre Boutillier, the point being that it
+is safe to propagate the information about structurally smaller
+arguments through $\beta$-redexes that are blocked by the
+``match'' construction (blocked commutative cuts).
+
+Relying on the added permissiveness of the guard condition, Hugo
+Herbelin could extend the pattern-matching compilation algorithm
+so that matching over a sequence of terms involving
+dependencies of a term or of the indices of the type of a term in the
+type of other terms is systematically supported.
+
+Regarding the high-level specification language, Pierre Boutillier
+introduced the ability to give implicit arguments to anonymous
+functions, Hugo Herbelin introduced the ability to define notations
+with several binders (e.g. \verb=exists x y z, P=), Matthieu Sozeau
+made the type classes inference mechanism more robust and predictable,
+Enrico Tassi introduced a command {\tt Arguments} that generalizes
+{\tt Implicit Arguments} and {\tt Arguments Scope} for assigning
+various properties to arguments of constants. Various improvements in
+the type inference algorithm were provided by Matthieu Sozeau and Hugo
+Herbelin with contributions from Enrico Tassi.
+
+Regarding tactics, Hugo Herbelin introduced support for referring to
+expressions occurring in the goal by pattern in tactics such as {\tt
+  set} or {\tt destruct}. Hugo Herbelin also relied on ideas from
+Chung-Kil Hur's {\tt Heq} plugin to introduce automatic computation of
+occurrences to generalize when using {\tt destruct} and {\tt
+  induction} on types with indices.  St\'ephane Glondu introduced new
+tactics {\tt constr\_eq}, {\tt is\_evar} and {\tt has\_evar} to be
+used when writing complex tactics.  Enrico Tassi added support to
+fine-tuning the behavior of {\tt simpl}. Enrico Tassi added the
+ability to specify over which variables of a section a lemma has
+to be exactly generalized.  Pierre Letouzey added a tactic {\tt
+  timeout} and the interruptibility of {\tt vm\_compute}.  Bug fixes
+and miscellaneous improvements of the tactic language came from Hugo
+Herbelin, Pierre Letouzey and Matthieu Sozeau.
+
+Regarding decision tactics, Lo\"ic Pottier maintained {\tt Nsatz},
+moving in particular to a type-class based reification of goals while
+Fr\'ed\'eric Besson maintained {\tt Micromega}, adding in particular
+support for division.
+
+Regarding vernacular commands, St\'ephane Glondu provided new commands
+to analyze the structure of type universes.
+
+Regarding libraries, a new library about lists of a given length
+(called vectors) has been provided by Pierre Boutillier. A new
+instance of finite sets based on Red-Black trees and provided by
+Andrew Appel has been adapted for the standard library by Pierre
+Letouzey. In the library of real analysis, Yves Bertot changed the
+definition of $\pi$ and provided a proof of the long-standing fact yet
+remaining unproved in this library, namely that $sin \frac{\pi}{2} =
+1$.
+
+Pierre Corbineau maintained the Mathematical Proof Language (C-zar).
+
+Bruno Barras and Benjamin Gr\'egoire maintained the call-by-value
+reduction machines.
+
+The extraction mechanism benefited from several improvements provided by
+Pierre Letouzey.
+
+Pierre Letouzey maintained the module system, with contributions from
+\'Elie Soubiran.
+
+Julien Forest maintained the {\tt Function} command.
+
+Matthieu Sozeau maintained the setoid rewriting mechanism.
+
+{\Coq} related tools have been upgraded too. In particular, {\tt
+  coq\_makefile} has been largely revised by Pierre Boutillier. Also,
+patches from Adam Chlipala for {\tt coqdoc} have been integrated by
+Pierre Boutillier.
+
+Bruno Barras and Pierre Letouzey maintained the {\tt coqchk} checker.
+
+Pierre Courtieu and Arnaud Spiwack contributed new features for using
+{\Coq} through Proof General.
+
+The {\tt Dp} plugin has been removed. Use the plugin provided with
+{\tt Why 3} instead (\url{http://why3.lri.fr}).
+
+Under the hood, the {\Coq} architecture benefited from improvements in
+terms of efficiency and robustness, especially regarding universes
+management and existential variables management, thanks to Pierre
+Letouzey and Yann R\'egis-Gianas with contributions from St\'ephane
+Glondu and Matthias Puech. The build system is maintained by Pierre
+Letouzey with contributions from St\'ephane Glondu and Pierre
+Boutillier.
+
+A new backtracking mechanism simplifying the task of external
+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.
+
+Packaging tools were provided by Pierre Letouzey (Windows), Pierre
+Boutillier (MacOS), St\'ephane Glondu (Debian). Releasing, testing and
+benchmarking support was provided by Jean-Marc Notin.
+
+Many suggestions for improvements were motivated by feedback from
+users, on either the bug tracker or the coq-club mailing list. Special
+thanks are going to the users who contributed patches, starting with
+Tom Prince. Other patch contributors include C\'edric Auger, David
+Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson,
+Hendrik Tews and Eelis van der Weegen.
+
+\begin{flushright}
+Paris, December 2011\\
+Hugo Herbelin\\
+\end{flushright}
+
+
+\section*{Credits: version 8.5}
+
+{\Coq} version 8.5 contains the result of five specific long-term
+projects:
+\begin{itemize}
+\item A new asynchronous evaluation and compilation mode by Enrico
+  Tassi with help from Bruno Barras and Carst Tankink.
+\item Full integration of the new proof engine by Arnaud Spiwack
+  helped by Pierre-Marie Pédrot,
+\item Addition of conversion and reduction based on native compilation
+  by Maxime Dénès and Benjamin Grégoire.
+\item Full universe polymorphism for definitions and inductive types by
+  Matthieu Sozeau.
+\item An implementation of primitive projections with $\eta$-conversion
+  bringing significant performance improvements when using records by
+  Matthieu Sozeau.
+\end{itemize}
+
+The full integration of the proof engine, by Arnaud Spiwack and
+Pierre-Marie Pédrot, brings to primitive tactics and the user level
+Ltac language dependent subgoals, deep backtracking and multiple goal
+handling, along with miscellaneous features and an improved potential
+for future modifications. Dependent subgoals allow statements in a
+goal to mention the proof of another. Proofs of unsolved subgoals
+appear as existential variables. Primitive backtracking makes it
+possible to write a tactic with several possible outcomes which are
+tried successively when subsequent tactics fail. Primitives are also
+available to control the backtracking behavior of tactics. Multiple
+goal handling paves the way for smarter automation tactics. It is
+currently used for simple goal manipulation such as goal reordering.
+
+The way {\Coq} processes a document in batch and interactive mode has
+been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
+proofs, the text between Proof and Qed, can be processed
+asynchronously, decoupling the checking of definitions and statements
+from the checking of proofs.  It improves the responsiveness of
+interactive development, since proofs can be processed in the
+background.  Similarly, compilation of a file can be split into two
+phases: the first one checking only definitions and statements and the
+second one checking proofs.  A file resulting from the first
+phase~--~with the .vio extension~--~can be already Required.  All .vio
+files can be turned into complete .vo files in parallel.  The same
+infrastructure also allows terminating tactics to be run in parallel
+on a set of goals via the \verb=par:= goal selector.
+
+{\CoqIDE} was modified to cope with asynchronous checking of the
+document.  Its source code was also made separate from that of {\Coq}, so
+that {\CoqIDE} no longer has a special status among user interfaces,
+paving the way for decoupling its release cycle from that of {\Coq} in
+the future.
+
+Carst Tankink developed a {\Coq} back-end for user interfaces built on
+Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
+help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander
+Faithfull and Jesper Bengtson).  The development of such features was
+funded by the Paral-ITP French ANR project.
+
+The full universe polymorphism extension was designed by Matthieu
+Sozeau. It conservatively extends the universes system and core calculus
+with definitions and inductive declarations parameterized by universes
+and constraints. It is based on a modification of the kernel architecture to
+handle constraint checking only, leaving the generation of constraints
+to the refinement/type inference engine. Accordingly, tactics are now
+fully universe aware, resulting in more localized error messages in case
+of inconsistencies and allowing higher-level algorithms like unification
+to be entirely type safe. The internal representation of universes has
+been modified but this is invisible to the user. 
+
+The underlying logic has been extended with $\eta$-conversion for
+records defined with primitive projections by Matthieu Sozeau. This
+additional form of $\eta$-conversion is justified using the same
+principle than the previously added $\eta$-conversion for function
+types, based on formulations of the Calculus of Inductive Constructions
+with typed equality. Primitive projections, which do not carry the
+parameters of the record and are rigid names (not defined as a
+pattern-matching construct), make working with nested records more
+manageable in terms of time and space consumption. This extension and
+universe polymorphism were carried out partly while Matthieu Sozeau was working
+at the IAS in Princeton.
+
+The guard condition has been made compliant with extensional equality
+principles such as propositional extensionality and univalence, thanks to
+Maxime Dénès and Bruno Barras. To ensure compatibility with the
+univalence axiom, a new flag ``-indices-matter'' has been implemented, 
+taking into account the universe levels of indices when computing the
+levels of inductive types. This supports using {\Coq} as a tool to explore
+the relations between homotopy theory and type theory.
+
+Maxime Dénès and Benjamin Grégoire developed an implementation of
+conversion test and normal form computation using the OCaml native
+compiler. It complements the virtual machine conversion offering much
+faster computation for expensive functions.
+
+{\Coq} 8.5 also comes with a bunch of many various smaller-scale
+changes and improvements regarding the different components of the
+system. We shall only list a few of them.
+
+Pierre Boutillier developed an improved tactic for simplification of
+expressions called {\tt cbn}.
+
+Maxime Dénès maintained the bytecode-based reduction machine. Pierre
+Letouzey maintained the extraction mechanism.
+
+Pierre-Marie Pédrot has extended the syntax of terms to,
+experimentally, allow holes in terms to be solved by a locally
+specified tactic.
+
+Existential variables are referred to by identifiers rather than mere
+numbers, thanks to Hugo Herbelin who also improved the tactic language
+here and there.
+
+Error messages for universe inconsistencies have been improved by
+Matthieu Sozeau. Error messages for unification and type inference
+failures have been improved by Hugo Herbelin, Pierre-Marie Pédrot and
+Arnaud Spiwack.
+
+Pierre Courtieu contributed new features for using {\Coq} through Proof
+General and for better interactive experience (bullets, Search, etc).
+
+The efficiency of the whole system has been significantly improved
+thanks to contributions from Pierre-Marie Pédrot.
+
+A distribution channel for {\Coq} packages using the OPAM tool has
+been initiated by Thomas Braibant and developed by Guillaume Claret,
+with contributions by Enrico Tassi and feedback from Hugo Herbelin.
+
+Packaging tools were provided by Pierre Letouzey and Enrico Tassi
+(Windows), Pierre Boutillier, Matthieu Sozeau and Maxime Dénès (MacOS
+X). Maxime Dénès improved significantly the testing and benchmarking
+support.
+
+Many power users helped to improve the design of the new features via
+the bug tracker, the coq development mailing list or the coq-club
+mailing list. Special thanks are going to the users who contributed
+patches and intensive brain-storming, starting with Jason Gross,
+Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson,
+Lionel Rieg. It would however be impossible to mention with precision
+all names of people who to some extent influenced the development.
+
+Version 8.5 is one of the most important release of {\Coq}. Its
+development spanned over about 3 years and a half with about one year
+of beta-testing. General maintenance during part or whole of this
+period has been done by Pierre Boutillier, Pierre Courtieu, Maxime
+Dénès, Hugo Herbelin, Pierre Letouzey, Guillaume Melquiond,
+Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi as
+well as Bruno Barras, Yves Bertot, Frédéric Besson, Xavier Clerc,
+Pierre Corbineau, Jean-Christophe Filliâtre, Julien Forest, Sébastien
+Hinderer, Assia Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François
+Ripault, Carst Tankink. Maxime Dénès coordinated the release process.
+
+\begin{flushright}
+Paris, January 2015, revised December 2015,\\
+Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
+\end{flushright}
+
+\section*{Credits: version 8.6}
+
+{\Coq} version 8.6 contains the result of refinements, stabilization of
+8.5's features and cleanups of the internals of the system. Over the
+year of (now time-based) development, about 450 bugs were resolved and
+over 100 contributions integrated. The main user visible changes are:
+\begin{itemize}
+\item A new, faster state-of-the-art universe constraint checker, by
+  Jacques-Henri Jourdan.
+\item In CoqIDE and other asynchronous interfaces, more fine-grained
+  asynchronous processing and error reporting by Enrico Tassi, making {\Coq}
+  capable of recovering from errors and continue processing the document.
+\item More access to the proof engine features from Ltac: goal
+  management primitives, range selectors and a {\tt typeclasses
+    eauto} engine handling multiple goals and multiple successes, by
+  Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.
+\item Tactic behavior uniformization and specification, generalization
+  of intro-patterns by Hugo Herbelin and others.
+\item A brand new warning system allowing to control warnings, turn them
+  into errors or ignore them selectively by Maxime Dénès, Guillaume
+  Melquiond, Pierre-Marie Pédrot and others.
+\item Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
+\item The {\tt ssreflect} subterm selection algorithm by Georges Gonthier and
+  Enrico Tassi is now accessible to tactic writers through the {\tt ssrmatching}
+  plugin.
+\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Jason
+  Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.
+\end{itemize}
+
+{\Coq} 8.6 also comes with a bunch of smaller-scale changes and
+improvements regarding the different components of the system. We shall
+only list a few of them.
+
+The {\tt iota} reduction flag is now a shorthand for {\tt match}, {\tt
+  fix} and {\tt cofix} flags controlling the corresponding reduction
+rules (by Hugo Herbelin and Maxime Dénès).
+
+Maxime Dénès maintained the native compilation machinery.
+
+Pierre-Marie Pédrot separated the Ltac code from general purpose
+tactics, and generalized and rationalized the handling of generic
+arguments, allowing to create new versions of Ltac more easily in the
+future.
+
+In patterns and terms, {\tt @}, abbreviations and notations are now
+interpreted the same way, by Hugo Herbelin.
+
+Name handling for universes has been improved by Pierre-Marie Pédrot and
+Matthieu Sozeau. The minimization algorithm has been improved by
+Matthieu Sozeau.
+
+The unifier has been improved by Hugo Herbelin and Matthieu Sozeau,
+fixing some incompatibilities introduced in Coq 8.5. Unification
+constraints can now be left floating around and be seen by the user
+thanks to a new option. The {\tt Keyed Unification} mode has been
+improved by Matthieu Sozeau. 
+
+The typeclass resolution engine and associated proof-search tactic have
+been reimplemented on top of the proof-engine monad, providing better
+integration in tactics, and new options have been introduced to control
+it, by Matthieu Sozeau with help from Théo Zimmermann.
+
+The efficiency of the whole system has been significantly improved
+thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and
+Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
+Steckler.
+
+Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre
+Letouzey and others.
+
+Emilio Jesús Gallego Arias contributed many cleanups and refactorings of
+the pretty-printing and user interface communication components.
+
+Frédéric Besson maintained the micromega tactic.
+
+The OPAM repository for {\Coq} packages has been maintained by Guillaume
+Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A
+list of packages is now available at \url{https://coq.inria.fr/opam/www/}.
+
+Packaging tools and software development kits were prepared by Michael
+Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and
+Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly
+built on the continuous integration server. {\Coq} now comes with a {\tt
+  META} file usable with {\tt ocamlfind}, contributed by Emilio Jesús
+Gallego Arias, Gregory Malecha, and Matthieu Sozeau.
+
+Matej Košík maintained and greatly improved the continuous integration
+setup and the testing of {\Coq} contributions. He also contributed many
+API improvement and code cleanups throughout the system.
+
+The contributors for this version are Bruno Barras, C.J. Bell, Yves
+Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume
+Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès,
+Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin,
+Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy,
+Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel,
+Guillaume Melquiond, Clément Pit--Claudel, Pierre-Marie Pédrot, Daniel
+de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote,
+Matthieu Sozeau, Arnaud Spiwack, Paul Steckler, Enrico Tassi, Laurent
+Théry, Nickolai Zeldovich and Théo Zimmermann. The development process
+was coordinated by Hugo Herbelin and Matthieu Sozeau with the help of
+Maxime Dénès, who was also in charge of the release process.
+
+Many power users helped to improve the design of the new features via
+the bug tracker, the pull request system, the {\Coq} development mailing
+list or the coq-club mailing list. Special thanks to the users who
+contributed patches and intensive brain-storming and code reviews,
+starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan
+Leivent, Xavier Leroy, Gregory Malecha, Clément Pit--Claudel, Gabriel
+Scherer and Beta Ziliani. It would however be impossible to mention
+exhaustively the names of everybody who to some extent influenced the
+development.
+
+Version 8.6 is the first release of {\Coq} developed on a time-based
+development cycle. Its development spanned 10 months from the release of
+{\Coq} 8.5 and was based on a public roadmap. To date, it contains more
+external contributions than any previous {\Coq} system. Code reviews
+were systematically done before integration of new features, with an
+important focus given to compatibility and performance issues, resulting
+in a hopefully more robust release than {\Coq} 8.5.
+
+Coq Enhancement Proposals (CEPs for short) were introduced by Enrico
+Tassi to provide more visibility and a discussion period on new
+features, they are publicly available \url{https://github.com/coq/ceps}.
+
+Started during this period, an effort is led by Yves Bertot and Maxime
+Dénès to put together a {\Coq} consortium.
+
+\begin{flushright}
+Paris, November 2016,\\
+Matthieu Sozeau and the {\Coq} development team\\
+\end{flushright}
+
+\section*{Credits: version 8.7}
+
+{\Coq} version 8.7 contains the result of refinements, stabilization of
+features and cleanups of the internals of the system along with a few
+new features. The main user visible changes are:
+\begin{itemize}
+\item New tactics: variants of tactics supporting existential variables
+  \texttt{eassert}, \texttt{eenough}, etc... by Hugo Herbelin. Tactics
+  \texttt{extensionality in H} and \texttt{inversion\_sigma} by Jason
+  Gross, \texttt{specialize with ...} accepting partial bindings by
+  Pierre Courtieu.
+\item Cumulative Polymorphic Inductive Types, allowing cumulativity of
+  universes to go through applied inductive types, by Amin Timany and
+  Matthieu Sozeau.
+\item Integration of the \texttt{SSReflect} plugin and its documentation in the
+  reference manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès.
+\item The \texttt{coq\_makefile} tool was completely redesigned to improve its
+  maintainability and the extensibility of generated Makefiles, and to
+  make \texttt{\_CoqProject} files more palatable to IDEs by Enrico Tassi.
+\end{itemize}
+
+{\Coq} 8.7 involved a large amount of work on cleaning and speeding up
+the code base, notably the work of Pierre-Marie Pédrot on making the
+tactic-level system insensitive to existential variable expansion,
+providing a safer API to plugin writers and making the code more
+robust. The \texttt{dev/doc/changes.txt} file documents the numerous
+changes to the implementation and improvements of interfaces. An effort
+to provide an official, streamlined API to plugin writers is in
+progress, thanks to the work of Matej Košík.
+
+Version 8.7 also comes with a bunch of smaller-scale changes and improvements
+regarding the different components of the system. We shall only list a
+few of them.
+
+The efficiency of the whole system has been significantly improved
+thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and
+Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
+Steckler.
+
+Thomas Sibut-Pinote and Hugo Herbelin added support for side effects
+hooks in \texttt{cbv}, \texttt{cbn} and \texttt{simpl}.  The side
+effects are provided via a plugin available at
+\url{https://github.com/herbelin/reduction-effects/}.
+
+The \texttt{BigN}, \texttt{BigZ}, \texttt{BigQ} libraries are no longer
+part of the {\Coq} standard library, they are now provided by a separate
+repository \url{https://github.com/coq/bignums}, maintained by Pierre
+Letouzey.
+
+In the \texttt{Reals} library, \texttt{IZR} has been changed to produce
+a compact representation of integers and real constants are now
+represented using \texttt{IZR} (work by Guillaume Melquiond).
+
+Standard library additions and improvements by Jason Gross, Pierre
+Letouzey and others, documented in the CHANGES file.
+
+The mathematical proof language/declarative mode plugin was removed from
+the archive.
+
+The OPAM repository for {\Coq} packages has been maintained by Guillaume
+Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many
+users. A list of packages is available at
+\url{https://coq.inria.fr/opam/www/}.
+
+Packaging tools and software development kits were prepared by Michael
+Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and
+Maxime Dénès for MacOS X. Packages are regularly built on the
+Travis continuous integration server.
+
+The contributors for this version are Abhishek Anand, C.J. Bell, Yves
+Bertot, Frédéric Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès,
+Julien Forest, Gaëtan Gilbert, Jason Gross, Hugo Herbelin, Emilio Jesús
+Gallego Arias, Ralf Jung, Matej Košík, Xavier Leroy, Pierre Letouzey,
+Assia Mahboubi, Cyprien Mangin, Erik Martin-Dorel, Olivier Marty,
+Guillaume Melquiond, Sam Pablo Kuper, Benjamin Pierce, Pierre-Marie
+Pédrot, Lars Rasmusson, Lionel Rieg, Valentin Robert, Yann Régis-Gianas,
+Thomas Sibut-Pinote, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack,
+Paul Steckler, George Stelle, Pierre-Yves Strub, Enrico Tassi, Hendrik
+Tews, Amin Timany, Laurent Théry, Vadim Zaliva and Théo Zimmermann.
+
+The development process was coordinated by Matthieu Sozeau with the help
+of Maxime Dénès, who was also in charge of the release process. Théo
+Zimmermann is the maintainer of this release.
+
+Many power users helped to improve the design of the new features via
+the bug tracker, the pull request system, the {\Coq} development mailing
+list or the coq-club mailing list. Special thanks to the users who
+contributed patches and intensive brain-storming and code reviews,
+starting with Jason Gross, Ralf Jung, Robbert Krebbers, Xavier Leroy,
+Clément Pit--Claudel and Gabriel Scherer. It would however be impossible
+to mention exhaustively the names of everybody who to some extent
+influenced the development.
+
+Version 8.7 is the second release of {\Coq} developed on a time-based
+development cycle. Its development spanned 9 months from the release of
+{\Coq} 8.6 and was based on a public road-map. It attracted many external
+contributions. Code reviews and continuous integration testing were
+systematically used before integration of new features, with an
+important focus given to compatibility and performance issues, resulting
+in a hopefully more robust release than {\Coq} 8.6 while maintaining
+compatibility.
+
+Coq Enhancement Proposals (CEPs for short) and open pull-requests
+discussions were used to discuss publicly the new features.
+
+The {\Coq} consortium, an organization directed towards users and
+supporters of the system, is now upcoming and will rely on Inria's
+newly created Foundation.
+
+\begin{flushright}
+Paris, August 2017,\\
+Matthieu Sozeau and the {\Coq} development team\\
+\end{flushright}
+
+
+%new Makefile
+
+%\newpage
+
+% Integration of ZArith lemmas from Sophia and Nijmegen.
+
+
+% $Id$ 
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: