Merge PR #6979: Sphinx doc credits

6 files changed, 1308 insertions, 1354 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 587c5ccbf..e6ab89efc 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -70,7 +70,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
   headers.sty Reference-Manual.tex \
-  RefMan-pre.tex RefMan-com.tex \
+  RefMan-com.tex \
   RefMan-uti.tex RefMan-ide.tex RefMan-modr.tex \
   AsyncProofs.tex RefMan-ssr.tex) \
   $(REFMANCOQTEXFILES) \
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
deleted file mode 100644
index 05775bfbe..000000000
--- a/doc/refman/RefMan-pre.tex
+++ /dev/null
@@ -1,1351 +0,0 @@
-%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: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 1bd79d511..4935b70c5 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -85,7 +85,6 @@ Options A and B of the licence are {\em not} elected.}
 %END LATEX
 
 %\defaultheaders
-\include{RefMan-pre}% Credits
 
 %BEGIN LATEX
 \tableofcontents
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 12aeee3f9..23bc9a2e4 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -95,7 +95,13 @@ language = None
 # List of patterns, relative to source directory, that match files and
 # directories to ignore when looking for source files.
 # This patterns also effect to html_static_path and html_extra_path
-exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store', 'introduction.rst']
+exclude_patterns = [
+  '_build',
+  'Thumbs.db',
+  '.DS_Store',
+  'introduction.rst',
+  'credits.rst'
+]
 
 # The reST default role (used for this markup: `text`) to use for all
 # documents.
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
new file mode 100644
index 000000000..e08b50f9e
--- /dev/null
+++ b/doc/sphinx/credits.rst
@@ -0,0 +1,1299 @@
+-------------------------------------------
+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
+*logical language* in which we write our axiomatizations and
+specifications, the *proof assistant* which allows the development of
+verified mathematical proofs, and the *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
+*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
+*types*. This effort culminated with *Principia Mathematica*, the first
+systematic attempt at a formal foundation of mathematics. A
+simplification of this system along the lines of simply typed
+:math:`\lambda`-calculus occurred with Church’s *Simple Theory of
+Types*. The :math:`\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 *Automath* project, the first full-scale attempt to develop and
+mechanically verify mathematical proofs. This effort culminated with
+Jutting’s verification of Landau’s *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öf’s *Intuitionistic Theory of Types*, attempts a new
+foundation of mathematics on constructive principles. The second one,
+Girard’s polymorphic :math:`\lambda`-calculus :math:`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 *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
+*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 *resolution*. Resolution relies on solving equations in free
+algebras (i.e. term structures), using the *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 *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 *programming logic*,
+based on extensions of Martin-Löf’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
+:math:`\lambda`-calculus, called the *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
+:math:`\lambda`-terms. A section mechanism, designed and implemented by
+G. Dowek, allowed hierarchical developments of mathematical theories.
+This high-level language was called the *Mathematical Vernacular*.
+Furthermore, an interactive *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 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:
+
+-  User-programmable tactics are allowed
+
+-  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
+
+-  A generic parsing scheme allows user-definable notations, with a
+   symmetric table-driven pretty-printer
+
+-  Syntactic definitions allow convenient abbreviations
+
+-  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.
+
+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ñoz implemented a decision procedure for intuitionistic propositional
+logic, based on results of R. Dyckhoff. J.C. Filliâ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”.
+
+| Rocquencourt, Feb. 1st 1995
+| Gérard Huet
+|
+
+Credits: addendum for version 6.1
+=================================
+
+The present version 6.1 of |Coq| is based on the V5.10 architecture. It
+was ported to the new language Objective Caml 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é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.
+
+| Lyon, Nov. 18th 1996
+| Christine Paulin
+|
+
+Credits: addendum for version 6.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âtre introduced a tactic for refining a goal, using
+a proof term with holes as a proof scheme.
+
+David Delahaye designed the 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âtre, Eduardo Giménez, Hugo Herbelin and Patrick
+Loiseleur.
+
+| Orsay, May 4th 1998
+| Christine Paulin
+|
+
+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 ``AutoRewrite`` tactic. He also designed the
+new behavior of ``Intro`` and provided the tacticals ``First`` and
+``Solve``.
+
+J.-C. Filliâtre developed the ``Correctness`` tactic.
+
+\E. Giménez extended the guard condition in fixpoints.
+
+H. Herbelin designed the new syntax for definitions and extended the
+``Induction`` tactic.
+
+P. Loiseleur developed the ``Quote`` tactic and the new design of the
+``Auto`` tactic, he also introduced the index of errors in the
+documentation.
+
+C. Paulin wrote the ``Focus`` command and introduced the reduction
+functions in definitions, this last feature was proposed by J.-F.
+Monin from CNET Lannion.
+
+| Orsay, Dec. 1999
+| Christine Paulin
+|
+
+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 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 Caml or 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 ``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 ``SearchPattern`` and ``SearchRewrite`` tools
+and the support for the pcoq interface
+(http://www-sop.inria.fr/lemme/pcoq/).
+
+Micaela Mayero and David Delahaye introduced Field, a decision tactic
+for commutative fields.
+
+Christine Paulin changed the elimination rules for empty and singleton
+propositional inductive types.
+
+Loïc Pottier developed Fourier, a tactic solving linear inequalities on
+real numbers.
+
+Pierre Crégut developed a new version based on reflexion of the 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
+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 Chrzszcz designed and implemented the module system of |Coq| whose
+foundations are in Judicaël Courant’s PhD thesis.
+
+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. 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.
+
+| Orsay, May. 2002
+| Hugo Herbelin & Christine Paulin
+|
+
+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 *impredicativity*
+of the sort 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 mathematics within classical logic. Moreover,
+even in an constructive setting, the impredicativity of 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 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
+
+-  a more uniform, purified style: all constructions are now lowercase,
+   with a functional programming perfume (e.g. abstraction is now
+   written fun), and more directly accessible to the novice (e.g.
+   dependent product is now written forall and allows omission of
+   types). Also, parentheses and are no longer mandatory for function
+   application.
+
+-  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.
+
+Together with the revision of the concrete syntax, a new mechanism of
+*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.
+
+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 Chrzszcz 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.
+
+| Palaiseau & Orsay, Apr. 2004
+| Hugo Herbelin & Christine Paulin
+| (updated Apr. 2006)
+|
+
+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 cvcl, Simplify and zenon. Hugo Herbelin
+implemented an experimental protocol for calling external tools from the
+tactic language.
+
+Matthieu Sozeau developed 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 Objective Caml”. 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 `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.
+
+| Palaiseau, July 2006
+| Hugo Herbelin
+|
+
+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 :math:`\mathbb{Z}`
+and :math:`\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 :math:`\mathbb{Q}` and :math:`\mathbb{R}`),
+Fourier-Motzkin with cutting planes (for linear systems in
+:math:`\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 :math:`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 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 coqdoc support, Vincent Siles contributed extensions of
+the Scheme command and of injection.
+
+Bruno Barras implemented the `coqchk` tool: this is a stand-alone
+type-checker that can be used to certify .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.
+
+| Palaiseau, June 2008
+| Hugo Herbelin
+|
+
+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 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 FSets and a new
+round of evolutions in the modular development of arithmetic (library
+Numbers). The reason for making 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 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 :math:`\mathbb{N}`,
+:math:`\mathbb{Z}` or :math:`\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
+:math:`\Delta`-equivalence, which respects as much as possible the names
+given by the users. He also designed with Pierre Letouzey a new
+convenient operator ``<+`` for nesting functor application, that
+provides a light notation for inheriting the properties of cascading
+modules.
+
+The new tactic nsatz is due to Loïc Pottier. It works by computing
+Gröbner 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 Program
+features (the Russell language). Pierre Letouzey maintained and improved
+the extraction mechanism. Bruno Barras and Élie Soubiran maintained the
+Coq checker, Julien Forest maintained the Function mechanism for
+reasoning over recursively defined functions. Matthieu Sozeau, Hugo
+Herbelin and Jean-Marc Notin maintained coqdoc. Frédéric Besson
+maintained the 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 (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.
+
+| Paris, April 2010
+| Hugo Herbelin
+|
+
+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 nat, N and BigN),
+positive arithmetic (type positive), integer arithmetic (Z and BigZ) and
+machine word arithmetic (type Int31). It provides with unified notations
+(e.g. systematic use of add and 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
+info and 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édrot
+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 :math:`\eta`-conversion
+thanks to Hugo Herbelin, Stéphane Glondu and Benjamin Grégoire. The
+addition of :math:`\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 :math:`\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. ``exists x y z, P``), Matthieu Sozeau made the
+type classes inference mechanism more robust and predictable, Enrico
+Tassi introduced a command Arguments that generalizes Implicit Arguments
+and 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 set or
+destruct. Hugo Herbelin also relied on ideas from Chung-Kil Hur’s Heq
+plugin to introduce automatic computation of occurrences to generalize
+when using destruct and induction on types with indices. Stéphane Glondu
+introduced new tactics constr\_eq, is\_evar and has\_evar to be used
+when writing complex tactics. Enrico Tassi added support to fine-tuning
+the behavior of 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 timeout and the interruptibility of
+vm\_compute. Bug fixes and miscellaneous improvements of the tactic
+language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau.
+
+Regarding decision tactics, Loïc Pottier maintained Nsatz, moving in
+particular to a type-class based reification of goals while Frédéric
+Besson maintained Micromega, adding in particular support for division.
+
+Regarding vernacular commands, Stéphane 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 :math:`\pi` and
+provided a proof of the long-standing fact yet remaining unproved in
+this library, namely that :math:`sin \frac{\pi}{2} =
+1`.
+
+Pierre Corbineau maintained the Mathematical Proof Language (C-zar).
+
+Bruno Barras and Benjamin Grégoire 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
+Élie Soubiran.
+
+Julien Forest maintained the Function command.
+
+Matthieu Sozeau maintained the setoid rewriting mechanism.
+
+Coq related tools have been upgraded too. In particular, coq\_makefile
+has been largely revised by Pierre Boutillier. Also, patches from Adam
+Chlipala for coqdoc have been integrated by Pierre Boutillier.
+
+Bruno Barras and Pierre Letouzey maintained the `coqchk` checker.
+
+Pierre Courtieu and Arnaud Spiwack contributed new features for using
+Coq through Proof General.
+
+The Dp plugin has been removed. Use the plugin provided with Why 3
+instead (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égis-Gianas with contributions from Stéphane Glondu
+and Matthias Puech. The build system is maintained by Pierre Letouzey
+with contributions from Stéphane 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éphane 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éphane 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édric Auger, David Baelde, Dan
+Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson, Hendrik Tews and
+Eelis van der Weegen.
+
+| Paris, December 2011
+| Hugo Herbelin
+|
+
+Credits: version 8.5
+====================
+
+Coq version 8.5 contains the result of five specific long-term projects:
+
+-  A new asynchronous evaluation and compilation mode by Enrico Tassi
+   with help from Bruno Barras and Carst Tankink.
+
+-  Full integration of the new proof engine by Arnaud Spiwack helped by
+   Pierre-Marie Pédrot,
+
+-  Addition of conversion and reduction based on native compilation by
+   Maxime Dénès and Benjamin Grégoire.
+
+-  Full universe polymorphism for definitions and inductive types by
+   Matthieu Sozeau.
+
+-  An implementation of primitive projections with
+   :math:`\eta`-conversion bringing significant performance improvements
+   when using records by Matthieu Sozeau.
+
+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 ``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 :math:`\eta`-conversion for
+records defined with primitive projections by Matthieu Sozeau. This
+additional form of :math:`\eta`-conversion is justified using the same
+principle than the previously added :math:`\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 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 releases 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.
+
+| Paris, January 2015, revised December 2015,
+| Hugo Herbelin, Matthieu Sozeau and the |Coq| development team
+|
+
+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:
+
+-  A new, faster state-of-the-art universe constraint checker, by
+   Jacques-Henri Jourdan.
+
+-  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.
+
+-  More access to the proof engine features from Ltac: goal management
+   primitives, range selectors and a typeclasses eauto engine handling
+   multiple goals and multiple successes, by Cyprien Mangin, Matthieu
+   Sozeau and Arnaud Spiwack.
+
+-  Tactic behavior uniformization and specification, generalization of
+   intro-patterns by Hugo Herbelin and others.
+
+-  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.
+
+-  Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
+
+-  The ssreflect subterm selection algorithm by Georges Gonthier and
+   Enrico Tassi is now accessible to tactic writers through the
+   ssrmatching plugin.
+
+-  Integration of LtacProf, a profiler for Ltac by Jason Gross, Paul
+   Steckler, Enrico Tassi and Tobias Tebbi.
+
+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 iota reduction flag is now a shorthand for match, fix and 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, @, 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 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 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 META
+file usable with 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 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.
+
+| Paris, November 2016,
+| Matthieu Sozeau and the |Coq| development team
+|
+
+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:
+
+- New tactics: variants of tactics supporting existential variables eassert,
+  eenough, etc... by Hugo Herbelin. Tactics extensionality in H and
+  inversion_sigma by Jason Gross, specialize with ... accepting partial bindings
+  by Pierre Courtieu.
+
+- Cumulative Polymorphic Inductive Types, allowing cumulativity of universes to
+  go through applied inductive types, by Amin Timany and Matthieu Sozeau.
+
+- Integration of the SSReflect plugin and its documentation in the reference
+  manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès.
+
+- The coq_makefile tool was completely redesigned to improve its maintainability
+  and the extensibility of generated Makefiles, and to make `_CoqProject` files
+  more palatable to IDEs by Enrico Tassi.
+
+|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 `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
+cbv, cbn and simpl. The side effects are provided via a plugin available at
+https://github.com/herbelin/reduction-effects/.
+
+The BigN, BigZ, BigQ libraries are no longer part of the |Coq| standard library,
+they are now provided by a separate repository https://github.com/coq/bignums,
+maintained by Pierre Letouzey.
+
+In the Reals library, `IZR` has been changed to produce a compact representation
+of integers and real constants are now represented using `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 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.
+
+| Paris, August 2017,
+| Matthieu Sozeau and the |Coq| development team
+|
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 7b8bc2bae..f5a57b9dd 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -7,6 +7,7 @@ Introduction
 ===========================================
 
 .. include:: introduction.rst
+.. include:: credits.rst
 
 ------------------
 Table of contents