Split credits chapter in two parts: history, and changelog in inverse chronological order.

4 files changed, 1521 insertions, 1515 deletions

diff --git a/doc/sphinx/credits.rst b/doc/sphinx/changes.rst
index 5873096523..6e560f68b8 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/changes.rst
@@ -1,1232 +1,505 @@
--------
-Credits
--------
-
-Historical roots
-----------------
-
-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 [#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
-λ-calculus occurred with Church’s *Simple Theory of
-Types*. The λ-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 λ-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 language, 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 semidecision 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.
-
-.. [#years] At the time of writting, i.e. 1995.
-
-Brief summary of the versions up to 5.10
-----------------------------------------
-
-.. note::
-   This summary was written in 1995 together with the previous
-   section and formed the initial version of the Credits chapter
-   (that has since then been appended to, at each new release).
-   A more comprehensive description of these early versions is
-   available in the next few sections, which were written in 2015.
-
-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
-λ-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
-λ-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-ends. 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
-|
-
-Version 1
----------
-
-.. note::
-
-   These additional notes come from a document written
-   in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin
-   to accompany their public release of the archive of versions 1.10 to 6.2
-   of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and
-   implemented in the Formel team, joint between the INRIA Rocquencourt
-   laboratory and the Ecole Normale Supérieure of Paris, from 1984
-   onwards.
-
-This software is a prototype type-checker for a higher-order logical
-formalism known as the Theory of Constructions, presented in his PhD
-thesis by Thierry Coquand, with influences from Girard's system F and
-de Bruijn's Automath.  The metamathematical analysis of the system is
-the PhD work of Thierry Coquand. The software is mostly the work of
-Gérard Huet.  Most of the mathematical examples verified with the
-software are due to Thierry Coquand.
-
-The programming language of the CONSTR software (as it was called at
-the time) was a version of ML adapted from the Edinburgh LCF system
-and running on a LISP backend. The main improvements from the original
-LCF ML were that ML was compiled rather than interpreted (Gérard Huet
-building on the original translator by Lockwood Morris), and that it
-was enriched by recursively defined types (work of Guy
-Cousineau). This ancestor of CAML was used and improved by Larry
-Paulson for his implementation of Cambridge LCF.
-
-Software developments of this prototype occurred from late 1983 to
-early 1985.
-
-Version 1.10 was frozen on December 22nd 1984. It is the version used
-for the examples in Thierry Coquand's thesis, defended on January 31st
-1985. There was a unique binding operator, used both for universal
-quantification (dependent product) at the level of types and
-functional abstraction (λ) at the level of terms/proofs, in the manner
-of Automath. Substitution (λ-reduction) was implemented using de
-Bruijn's indexes.
-
-Version 1.11 was frozen on February 19th, 1985. It is the version used
-for the examples in the paper: T. Coquand, G. Huet. *Constructions: A
-Higher Order Proof System for Mechanizing Mathematics* :cite:`CH85`.
-
-Christine Paulin joined the team at this point, for her DEA research
-internship.  In her DEA memoir (August 1985) she presents developments
-for the *lambo* function – :math:`\text{lambo}(f)(n)` computes the minimal
-:math:`m` such that :math:`f(m)` is greater than :math:`n`, for :math:`f`
-an increasing integer function, a challenge for constructive mathematics.
-She also encoded the majority voting algorithm of Boyer and Moore.
-
-Version 2
----------
-
-The formal system, now renamed as the *Calculus of Constructions*, was
-presented with a proof of consistency and comparisons with proof
-systems of Per Martin Löf, Girard, and the Automath family of N. de
-Bruijn, in the paper: T. Coquand and G. Huet. *The Calculus of
-Constructions* :cite:`CH88`.
-
-An abstraction of the software design, in the form of an abstract
-machine for proof checking, and a fuller sequence of mathematical
-developments was presented in: T. Coquand, G. Huet. *Concepts
-Mathématiques et Informatiques Formalisés dans le Calcul des
-Constructions* :cite:`CH87`.
-
-Version 2.8 was frozen on December 16th, 1985, and served for
-developing the examples in the above papers.
-
-This calculus was then enriched in version 2.9 with a cumulative
-hierarchy of universes. Universe levels were initially explicit
-natural numbers.  Another improvement was the possibility of automatic
-synthesis of implicit type arguments, relieving the user of tedious
-redundant declarations.
-
-Christine Paulin wrote an article *Algorithm development in the
-Calculus of Constructions* :cite:`P86`. Besides *lambo* and *majority*,
-she presents *quicksort* and a text formatting algorithm.
-
-Version 2.13 of the Calculus of Constructions with universes was
-frozen on June 25th, 1986.
-
-A synthetic presentation of type theory along constructive lines with
-ML algorithms was given by Gérard Huet in his May 1986 CMU course
-notes *Formal Structures for Computation and Deduction*. Its chapter
-*Induction and Recursion in the Theory of Constructions* was presented
-as an invited paper at the Joint Conference on Theory and Practice of
-Software Development TAPSOFT’87 at Pise in March 1987, and published
-as *Induction Principles Formalized in the Calculus of
-Constructions* :cite:`H88`.
-
-Version 3
----------
-
-This version saw the beginning of proof automation, with a search
-algorithm inspired from PROLOG and the applicative logic programming
-programs of the course notes *Formal structures for computation and
-deduction*.  The search algorithm was implemented in ML by Thierry
-Coquand.  The proof system could thus be used in two modes: proof
-verification and proof synthesis, with tactics such as ``AUTO``.
-
-The implementation language was now called CAML, for Categorical
-Abstract Machine Language. It used as backend the LLM3 virtual machine
-of Le Lisp by Jérôme Chailloux. The main developers of CAML were
-Michel Mauny, Ascander Suarez and Pierre Weis.
-
-V3.1 was started in the summer of 1986, V3.2 was frozen at the end of
-November 1986. V3.4 was developed in the first half of 1987.
-
-Thierry Coquand held a post-doctoral position in Cambrige University
-in 1986-87, where he developed a variant implementation in SML, with
-which he wrote some developments on fixpoints in Scott's domains.
-
-Version 4
----------
-
-This version saw the beginning of program extraction from proofs, with
-two varieties of the type ``Prop`` of propositions, indicating
-constructive intent.  The proof extraction algorithms were implemented
-by Christine Paulin-Mohring.
-
-V4.1 was frozen on July 24th, 1987. It had a first identified library
-of mathematical developments (directory ``exemples``), with libraries
-``Logic`` (containing impredicative encodings of intuitionistic logic and
-algebraic primitives for booleans, natural numbers and list), ``Peano``
-developing second-order Peano arithmetic, ``Arith`` defining addition,
-multiplication, euclidean division and factorial. Typical developments
-were the Knaster-Tarski theorem and Newman's lemma from rewriting
-theory.
-
-V4.2 was a joint development of a team consisting of Thierry Coquand,
-Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the
-log of changes.  It was frozen on September 1987 as the last version
-implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable
-development system.
-
-V4.3 saw the first top-level of the system. Instead of evaluating
-explicit quotations, the user could develop his mathematics in a
-high-level language called the mathematical vernacular (following
-Automath terminology).  The user could develop files in the vernacular
-notation (with ``.v`` extension) which were now separate from the ``ml``
-sources of the implementation.  Gilles Dowek joined the team to
-develop the vernacular language as his DEA internship research.
-
-A notion of sticky constant was introduced, in order to keep names of
-lemmas when local hypotheses of proofs were discharged. This gave a
-notion of global mathematical environment with local sections.
-
-Another significant practical change was that the system, originally
-developped on the VAX central computer of our lab, was transferred on
-SUN personal workstations, allowing a level of distributed
-development.  The extraction algorithm was modified, with three
-annotations ``Pos``, ``Null`` and ``Typ`` decorating the sorts ``Prop``
-and ``Type``.
-
-Version 4.3 was frozen at the end of November 1987, and was
-distributed to an early community of users (among those were Hugo
-Herbelin and Loic Colson).
-
-V4.4 saw the first version of (encoded) inductive types.  Now natural
-numbers could be defined as::
-
-  [source, coq]
-  Inductive NAT : Prop = O : NAT | Succ : NAT->NAT.
-
-These inductive types were encoded impredicatively in the calculus,
-using a subsystem *rec* due to Christine Paulin.  V4.4 was frozen on
-March 6th 1988.
-
-Version 4.5 was the first one to support inductive types and program
-extraction.  Its banner was *Calcul des Constructions avec
-Réalisations et Synthèse*.  The vernacular language was enriched to
-accommodate extraction commands.
-
-The verification engine design was presented as: G. Huet. *The
-Constructive Engine*. Version 4.5. Invited Conference, 2nd European
-Symposium on Programming, Nancy, March 88.  The final paper,
-describing the V4.9 implementation, appeared in: A perspective in
-Theoretical Computer Science, Commemorative Volume in memory of Gift
-Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.
-
-Version 4.5 was demonstrated in June 1988 at the YoP Institute on
-Logical Foundations of Functional Programming organized by Gérard Huet
-at Austin, Texas.
-
-Version 4.6 was started during the summer of 1988. Its main
-improvement was the complete rehaul of the proof synthesis engine by
-Thierry Coquand, with a tree structure of goals.
-
-Its source code was communicated to Randy Pollack on September 2nd
-1988.  It evolved progressively into LEGO, proof system for Luo's
-formalism of Extended Calculus of Constructions.
-
-The discharge tactic was modified by Gérard Huet to allow for
-inter-dependencies in discharged lemmas. Christine Paulin improved the
-inductive definition scheme in order to accommodate predicates of any
-arity.
-
-Version 4.7 was started on September 6th, 1988.
-
-This version starts exploiting the CAML notion of module in order to
-improve the modularity of the implementation. Now the term verifier is
-identified as a proper module Machine, which the structure of its
-internal data structures being hidden and thus accessible only through
-the legitimate operations.  This machine (the constructive engine) was
-the trusted core of the implementation. The proof synthesis mechanism
-was a separate proof term generator. Once a complete proof term was
-synthesized with the help of tactics, it was entirely re-checked by
-the engine. Thus there was no need to certify the tactics, and the
-system took advantage of this fact by having tactics ignore the
-universe levels, universe consistency check being relegated to the
-final type-checking pass. This induced a certain puzzlement in early
-users who saw, after a successful proof search, their ``QED`` followed
-by silence, followed by a failure message due to a universe
-inconsistency…
-
-The set of examples comprise set theory experiments by Hugo Herbelin,
-and notably the Schroeder-Bernstein theorem.
-
-Version 4.8, started on October 8th, 1988, saw a major
-re-implementation of the abstract syntax type ``constr``, separating
-variables of the formalism and metavariables denoting incomplete terms
-managed by the search mechanism.  A notion of level (with three values
-``TYPE``, ``OBJECT`` and ``PROOF``) is made explicit and a type judgement
-clarifies the constructions, whose implementation is now fully
-explicit. Structural equality is speeded up by using pointer equality,
-yielding spectacular improvements. Thierry Coquand adapts the proof
-synthesis to the new representation, and simplifies pattern matching
-to first-order predicate calculus matching, with important performance
-gain.
-
-A new representation of the universe hierarchy is then defined by
-Gérard Huet.  Universe levels are now implemented implicitly, through
-a hidden graph of abstract levels constrained with an order relation.
-Checking acyclicity of the graph insures well-foundedness of the
-ordering, and thus consistency. This was documented in a memo *Adding
-Type:Type to the Calculus of Constructions* which was never published.
-
-The development version is released as a stable 4.8 at the end of
-1988.
-
-Version 4.9 is released on March 1st 1989, with the new "elastic"
-universe hierarchy.
-
-The spring of 1989 saw the first attempt at documenting the system
-usage, with a number of papers describing the formalism:
-
-- *Metamathematical Investigations of a Calculus of Constructions*, by
-  Thierry Coquand :cite:`C90`,
-
-- *Inductive definitions in the Calculus of Constructions*, by
-  Christine Paulin-Mohrin,
-
-- *Extracting Fω's programs from proofs in the Calculus of
-  Constructions*, by Christine Paulin-Mohring* :cite:`P89`,
-
-- *The Constructive Engine*, by Gérard Huet :cite:`H89`,
-
-as well as a number of user guides:
-
-- *A short user's guide for the Constructions*, Version 4.10, by Gérard Huet
-- *A Vernacular Syllabus*, by Gilles Dowek.
-- *The Tactics Theorem Prover, User's guide*, Version 4.10, by Thierry
-  Coquand.
-
-Stable V4.10, released on May 1st, 1989, was then a mature system,
-distributed with CAML V2.6.
-
-In the mean time, Thierry Coquand and Christine Paulin-Mohring had
-been investigating how to add native inductive types to the Calculus
-of Constructions, in the manner of Per Martin-Löf's Intuitionistic
-Type Theory. The impredicative encoding had already been presented in:
-F. Pfenning and C. Paulin-Mohring. *Inductively defined types in the
-Calculus of Constructions* :cite:`PP90`. An extension of the calculus
-with primitive inductive types appeared in: T. Coquand and
-C. Paulin-Mohring. *Inductively defined types* :cite:`CP90`.
-
-This led to the Calculus of Inductive Constructions, logical formalism
-implemented in Versions 5 upward of the system, and documented in:
-C. Paulin-Mohring. *Inductive Definitions in the System Coq - Rules
-and Properties* :cite:`P93`.
-
-The last version of CONSTR is Version 4.11, which was last distributed
-in the spring of 1990. It was demonstrated at the first workshop of
-the European Basic Research Action Logical Frameworks In Sophia
-Antipolis in May 1990.
-
-Version 5
----------
-
-At the end of 1989, Version 5.1 was started, and renamed as the system
-Coq for the Calculus of Inductive Constructions. It was then ported to
-the new stand-alone implementation of ML called Caml-light.
-
-In 1990 many changes occurred. Thierry Coquand left for Chalmers
-University in Göteborg. Christine Paulin-Mohring took a CNRS
-researcher position at the LIP laboratory of École Normale Supérieure
-de Lyon. Project Formel was terminated, and gave rise to two teams:
-Cristal at INRIA-Roquencourt, that continued developments in
-functional programming with Caml-light then OCaml, and Coq, continuing
-the type theory research, with a joint team headed by Gérard Huet at
-INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory
-of CNRS-ENS Lyon.
-
-Chetan Murthy joined the team in 1991 and became the main software
-architect of Version 5. He completely rehauled the implementation for
-efficiency.  Versions 5.6 and 5.8 were major distributed versions,
-with complete documentation and a library of users' developements. The
-use of the RCS revision control system, and systematic ChangeLog
-files, allow a more precise tracking of the software developments.
-
-| September 2015 +
-| Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.
-|
-
-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
-|
+--------------
+Recent changes
+--------------
 
-Version 6.2
+Version 8.9
 -----------
 
-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 reduction 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 the 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
-|
-
-Version 6.3
------------
+|Coq| version 8.9 contains the result of refinements and stabilization
+of features and deprecations or removals of deprecated features,
+cleanups of the internals of the system and API along with a few new
+features. This release includes many user-visible changes, including
+deprecations that are documented in ``CHANGES.md`` and new features that
+are documented in the reference manual. Here are the most important
+changes:
 
-The main changes in version V6.3 were the introduction of a few new
-tactics and the extension of the guard condition for fixpoint
-definitions.
+- Kernel: mutually recursive records are now supported, by Pierre-Marie
+  Pédrot.
 
-B. Barras extended the unification algorithm to complete partial terms
-and fixed various tricky bugs related to universes.
+- Notations:
 
-D. Delahaye developed the ``AutoRewrite`` tactic. He also designed the
-new behavior of ``Intro`` and provided the tacticals ``First`` and
-``Solve``.
+  - Support for autonomous grammars of terms called “custom entries”, by
+    Hugo Herbelin (see Section :ref:`custom-entries` of the reference
+    manual).
 
-J.-C. Filliâtre developed the ``Correctness`` tactic.
+  - Deprecated notations of the standard library will be removed in the
+    next version of |Coq|, see the ``CHANGES.md`` file for a script to
+    ease porting, by Jason Gross and Jean-Christophe Léchenet.
 
-\E. Giménez extended the guard condition in fixpoints.
+  - Added the :cmd:`Numeral Notation` command for registering decimal
+    numeral notations for custom types, by Daniel de Rauglaudre, Pierre
+    Letouzey and Jason Gross.
 
-H. Herbelin designed the new syntax for definitions and extended the
-``Induction`` tactic.
+- Tactics: Introduction tactics :tacn:`intro`/:tacn:`intros` on a goal that is an
+  existential variable now force a refinement of the goal into a
+  dependent product rather than failing, by Hugo Herbelin.
 
-P. Loiseleur developed the ``Quote`` tactic and the new design of the
-``Auto`` tactic, he also introduced the index of errors in the
-documentation.
+- Decision procedures: deprecation of tactic ``romega`` in favor of
+  :tacn:`lia` and removal of ``fourier``, replaced by :tacn:`lra` which
+  subsumes it, by Frédéric Besson, Maxime Dénès, Vincent Laporte and
+  Laurent Théry.
 
-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.
+- Proof language: focusing bracket ``{`` now supports named
+  :ref:`goals <curly-braces>`, e.g. ``[x]:{`` will focus
+  on a goal (existential variable) named ``x``, by Théo Zimmermann.
 
-| Orsay, Dec. 1999
-| Christine Paulin
-|
+- SSReflect: the implementation of delayed clear was simplified by
+  Enrico Tassi: the variables are always renamed using inaccessible
+  names when the clear switch is processed and finally cleared at the
+  end of the intro pattern. In addition to that, the use-and-discard flag
+  ``{}`` typical of rewrite rules can now be also applied to views,
+  e.g. ``=> {}/v`` applies ``v`` and then clears ``v``. See Section
+  :ref:`introduction_ssr`.
 
-Versions 7
-----------
+- Vernacular:
 
-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.
+  - Experimental support for :ref:`attributes <gallina-attributes>` on
+    commands, by Vincent Laporte, as in ``#[local] Lemma foo : bar.``
+    Tactics and tactic notations now support the ``deprecated``
+    attribute.
 
-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.
+  - Removed deprecated commands ``Arguments Scope`` and ``Implicit
+    Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper
+    Hugunin.
 
-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.
+  - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to
+    avoid repeating uniform parameters in constructor declarations.
 
-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.
+  - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by
+    Matthieu Sozeau, for controlling the opacity status of variables and
+    constants in hint databases. It is recommended to always use these
+    commands after creating a hint databse with :cmd:`Create HintDb`.
 
-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.
+  - Multiple sections with the same name are now allowed, by Jasper
+    Hugunin.
 
-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.
+- Library: additions and changes in the ``VectorDef``, ``Ascii``, and
+  ``String`` libraries. Syntax notations are now available only when using
+  ``Import`` of libraries and not merely ``Require``, by various
+  contributors (source of incompatibility, see ``CHANGES.md`` for details).
 
-Bruno Barras improved the efficiency of the reduction algorithm and the
-confidence level in the correctness of |Coq| critical type checking
-algorithm.
+- Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof
+  steps in color, using the :opt:`Diffs` option, by Jim Fehrle.
 
-Yves Bertot designed the ``SearchPattern`` and ``SearchRewrite`` tools
-and the support for the pcoq interface
-(http://www-sop.inria.fr/lemme/pcoq/).
+- Documentation: we integrated a large number of fixes to the new Sphinx
+  documentation by various contributors, coordinated by Clément
+  Pit-Claudel and Théo Zimmermann.
 
-Micaela Mayero and David Delahaye introduced Field, a decision tactic
-for commutative fields.
+- Tools: removed the ``gallina`` utility and the homebrewed ``Emacs`` mode.
 
-Christine Paulin changed the elimination rules for empty and singleton
-propositional inductive types.
+- Packaging: as in |Coq| 8.8.2, the Windows installer now includes many
+  more external packages that can be individually selected for
+  installation, by Michael Soegtrop.
 
-Loïc Pottier developed Fourier, a tactic solving linear inequalities on
-real numbers.
+Version 8.9 also comes with a bunch of smaller-scale changes and
+improvements regarding the different components of the system.  Most
+important ones are documented in the ``CHANGES.md`` file.
 
-Pierre Crégut developed a new, reflection-based version of the Omega
-decision procedure.
+On the implementation side, the ``dev/doc/changes.md`` file documents
+the numerous changes to the implementation and improvements of
+interfaces. The file provides guidelines on porting a plugin to the new
+version and a plugin development tutorial kept in sync with Coq was
+introduced by Yves Bertot http://github.com/ybertot/plugin_tutorials.
+The new ``dev/doc/critical-bugs`` file documents the known critical bugs
+of |Coq| and affected releases.
 
-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).
+The efficiency of the whole system has seen improvements thanks to
+contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès.
 
-A library for efficient representation of finite maps using binary trees
-contributed by Jean Goubault was integrated in the basic theories.
+Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
+Soegtrop, Théo Zimmermann worked on maintaining and improving the
+continuous integration system.
 
-Pierre Courtieu developed a command and a tactic to reason on the
-inductive structure of recursively defined functions.
+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/.
 
-Jacek Chrząszcz designed and implemented the module system of |Coq| whose
-foundations are in Judicaël Courant’s PhD thesis.
+The 54 contributors for this version are Léo Andrès, Rin Arakaki,
+Benjamin Barenblat, Langston Barrett, Siddharth Bhat, Martin Bodin,
+Simon Boulier, Timothy Bourke, Joachim Breitner, Tej Chajed, Arthur
+Charguéraud, Pierre Courtieu, Maxime Dénès, Andres Erbsen, Jim Fehrle,
+Julien Forest, Emilio Jesus Gallego Arias, Gaëtan Gilbert, Matěj
+Grabovský, Jason Gross, Samuel Gruetter, Armaël Guéneau, Hugo Herbelin,
+Jasper Hugunin, Ralf Jung, Sam Pablo Kuper, Ambroise Lafont, Leonidas
+Lampropoulos, Vincent Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey,
+Jean-Christophe Léchenet, Nick Lewycky, Yishuai Li, Sven M. Hallberg,
+Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Perry E. Metzger,
+Clément Pit-Claudel, Pierre-Marie Pédrot, Daniel R. Grayson, Kazuhiko
+Sakaguchi, Michael Soegtrop, Matthieu Sozeau, Paul Steckler, Enrico
+Tassi, Laurent Théry, Anton Trunov, whitequark, Théo Winterhalter,
+Zeimer, Beta Ziliani, Théo Zimmermann.
 
-The development was coordinated by C. Paulin.
+Many power users helped to improve the design of the new features via
+the issue and pull request system, the |Coq| development mailing list or
+the coq-club@inria.fr mailing list. It would be impossible to mention
+exhaustively the names of everybody who to some extent influenced the
+development.
 
-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.
+Version 8.9 is the fourth release of |Coq| developed on a time-based
+development cycle. Its development spanned 7 months from the release of
+|Coq| 8.8. The development moved to a decentralized merging process
+during this cycle. Guillaume Melquiond was in charge of the release
+process and is the maintainer of this release. This release is the
+result of ~2,000 commits and ~500 PRs merged, closing 75+ issues.
 
-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.
+The |Coq| development team welcomed Vincent Laporte, a new |Coq|
+engineer working with Maxime Dénès in the |Coq| consortium.
 
-| Orsay, May. 2002
-| Hugo Herbelin & Christine Paulin
+| Paris, November 2018,
+| Matthieu Sozeau for the |Coq| development team
 |
 
-Version 8.0
+Version 8.8
 -----------
 
-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 are no longer mandatory for function
-   application.
+|Coq| version 8.8 contains the result of refinements and stabilization of
+features and deprecations, cleanups of the internals of the system along
+with a few new features. The main user visible changes are:
 
--  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.
+- Kernel: fix a subject reduction failure due to allowing fixpoints
+  on non-recursive values, by Matthieu Sozeau.
+  Handling of evars in the VM (the kernel still does not accept evars)
+  by Pierre-Marie Pédrot.
 
-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.
+- Notations: many improvements on recursive notations and support for
+  destructuring patterns in the syntax of notations by Hugo Herbelin.
 
-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.
+- Proof language: tacticals for profiling, timing and checking success
+  or failure of tactics by Jason Gross. The focusing bracket ``{``
+  supports single-numbered goal selectors, e.g. ``2:{``, by Théo
+  Zimmermann.
 
-Thirdly, a restructuring and uniformization 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.
+- Vernacular: deprecation of commands and more uniform handling of the
+  ``Local`` flag, by Vincent Laporte and Maxime Dénès, part of a larger
+  attribute system overhaul. Experimental ``Show Extraction`` command by
+  Pierre Letouzey. Coercion now accepts ``Prop`` or ``Type`` as a source
+  by Arthur Charguéraud. ``Export`` modifier for options allowing to
+  export the option to modules that ``Import`` and not only ``Require``
+  a module, by Pierre-Marie Pédrot.
 
-The fourth point is the release of |CoqIDE|, a new graphical gtk2-based
-interface fully integrated with |Coq|. Close in style to 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|.
+- Universes: many user-level and API level enhancements: qualified
+  naming and printing, variance annotations for cumulative inductive
+  types, more general constraints and enhancements of the minimization
+  heuristics, interaction with modules by Gaëtan Gilbert, Pierre-Marie
+  Pédrot and Matthieu Sozeau.
 
-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.
+- Library: Decimal Numbers library by Pierre Letouzey and various small
+  improvements.
 
-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.
+- Documentation: a large community effort resulted in the migration
+  of the reference manual to the Sphinx documentation tool. The result
+  is this manual. The new documentation infrastructure (based on Sphinx)
+  is by Clément Pit-Claudel. The migration was coordinated by Maxime Dénès
+  and Paul Steckler, with some help of Théo Zimmermann during the
+  final integration phase. The 14 people who ported the manual are
+  Calvin Beck, Heiko Becker, Yves Bertot, Maxime Dénès, Richard Ford,
+  Pierre Letouzey, Assia Mahboubi, Clément Pit-Claudel,
+  Laurence Rideau, Matthieu Sozeau, Paul Steckler, Enrico Tassi,
+  Laurent Théry, Nikita Zyuzin.
 
-Bruno Barras and Hugo Herbelin have been the main contributors of the
-reflection 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.
+- Tools: experimental ``-mangle-names`` option to ``coqtop``/``coqc`` for
+  linting proof scripts, by Jasper Hugunin.
 
-Hugo Herbelin is the main designer and implementer of the notion of
-interpretation scopes and of the commands for easily adding new
-notations.
+On the implementation side, the ``dev/doc/changes.md`` file
+documents the numerous changes to the implementation and improvements of
+interfaces. The file provides guidelines on porting a plugin to the new
+version.
 
-Hugo Herbelin is the main implementer of the restructured standard library.
+Version 8.8 also comes with a bunch of smaller-scale changes and
+improvements regarding the different components of the system.
+Most important ones are documented in the ``CHANGES.md`` file.
 
-Pierre Corbineau is the main designer and implementer 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.
+The efficiency of the whole system has seen improvements thanks to
+contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and
+Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
+Steckler.
 
-Benjamin Monate is the developer of the |CoqIDE| graphical interface with
-contributions by Jean-Christophe Filliâtre, Pierre Letouzey, Claude
-Marché and Bruno Barras.
+The official wiki and the bugtracker of |Coq| migrated to the GitHub
+platform, thanks to the work of Pierre Letouzey and Théo
+Zimmermann. Gaëtan Gilbert, Emilio Jesús Gallego Arias worked on
+maintaining and improving the continuous integration system.
 
-Claude Marché coordinated the edition of the Reference Manual for |Coq|
-V8.0.
+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/.
 
-Pierre Letouzey and Jacek Chrząszcz respectively maintained the
-extraction tool and module system of |Coq|.
+The 44 contributors for this version are Yves Bertot, Joachim Breitner, Tej
+Chajed, Arthur Charguéraud, Jacques-Pascal Deplaix, Maxime Dénès, Jim Fehrle,
+Julien Forest, Yannick Forster, Gaëtan Gilbert, Jason Gross, Samuel Gruetter,
+Thomas Hebb, Hugo Herbelin, Jasper Hugunin, Emilio Jesus Gallego Arias, Ralf
+Jung, Johannes Kloos, Matej Košík, Robbert Krebbers, Tony Beta Lambda, Vincent
+Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey, Farzon Lotfi, Cyprien Mangin,
+Guillaume Melquiond, Raphaël Monat, Carl Patenaude Poulin, Pierre-Marie Pédrot,
+Clément Pit-Claudel, Matthew Ryan, Matt Quinn, Sigurd Schneider, Bernhard
+Schommer, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack, Paul Steckler,
+Enrico Tassi, Anton Trunov, Martin Vassor, Vadim Zaliva and Théo Zimmermann.
 
-Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other
-contributors from Sophia-Antipolis and Nijmegen participated in
-extending the library.
+Version 8.8 is the third release of |Coq| developed on a time-based
+development cycle. Its development spanned 6 months from the release of
+|Coq| 8.7 and was based on a public roadmap. The development process
+was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the
+release process. Théo Zimmermann is the maintainer of this release.
 
-Julien Narboux built a NSIS-based automatic |Coq| installation tool for
-the Windows platform.
+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@inria.fr 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 and Amin Timany.
+It would however be impossible to mention exhaustively the names
+of everybody who to some extent influenced the development.
 
-Hugo Herbelin and Christine Paulin coordinated the development which was
-under the responsibility of Christine Paulin.
+The |Coq| consortium, an organization directed towards users and
+supporters of the system, is now running and employs Maxime Dénès.
+The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès.
 
-| Palaiseau & Orsay, Apr. 2004
-| Hugo Herbelin & Christine Paulin
-| (updated Apr. 2006)
+| Santiago de Chile, March 2018,
+| Matthieu Sozeau for the |Coq| development team
 |
 
-Version 8.1
+Version 8.7
 -----------
 
-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 for rings and
-semirings.
-
-Laurent Théry and Bruno Barras developed a new, significantly more
-efficient simplification algorithm for 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.
+|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:
 
-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.
+- New tactics: variants of tactics supporting existential variables :tacn:`eassert`,
+  :tacn:`eenough`, etc... by Hugo Herbelin. Tactics ``extensionality in H`` and
+  :tacn:`inversion_sigma` by Jason Gross, ``specialize with ...`` accepting partial bindings
+  by Pierre Courtieu.
 
-Pierre Corbineau extended his tactic for solving first-order statements.
-He wrote a reflection-based intuitionistic tautology solver.
+- ``Cumulative Polymorphic Inductive`` types, allowing cumulativity of universes to
+  go through applied inductive types, by Amin Timany and Matthieu Sozeau.
 
-Pierre Courtieu, Julien Forest and Yves Bertot added extra support to
-reason on the inductive structure of recursively defined functions.
+- Integration of the SSReflect plugin and its documentation in the reference
+  manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès.
 
-Jean-Marc Notin significantly contributed to the general maintenance of
-the system. He also took care of ``coqdoc``.
+- 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.
 
-Pierre Castéran contributed to the documentation of (co-)inductive types
-and suggested improvements to the libraries.
+|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.
 
-Pierre Corbineau implemented a declarative mathematical proof language,
-usable in combination with the tactic-based style of proof.
+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.
 
-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.
+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.
 
-| Palaiseau, July 2006
-| Hugo Herbelin
-|
+Thomas Sibut-Pinote and Hugo Herbelin added support for side effect hooks in
+cbv, cbn and simpl. The side effects are provided via a plugin available at
+https://github.com/herbelin/reduction-effects/.
 
-Version 8.2
------------
+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.
 
-Coq version 8.2 adds new features, new libraries and improves on many
-various aspects.
+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).
 
-Regarding the language of |Coq|, the main novelty is the introduction by
-Matthieu Sozeau of a package of commands providing Haskell-style typeclasses.
-Typeclasses, which come with a few convenient features such as
-type-based resolution of implicit arguments, play a new landmark role
-in the architecture of |Coq| with respect to automation. For
-instance, thanks to typeclass support, Matthieu Sozeau could
-implement a new resolution-based version of the tactics dedicated to
-rewriting on arbitrary transitive relations.
+Standard library additions and improvements by Jason Gross, Pierre Letouzey and
+others, documented in the ``CHANGES.md`` file.
 
-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 arithmetic 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 automation in
-presence of various number-theory concepts.
+The mathematical proof language/declarative mode plugin was removed from the
+archive.
 
-Frédéric Besson contributed a reflective 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.
+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/.
 
-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 arithmetic for efficiently computing
-with the library of integers he developed.
+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.
 
-Beside the libraries, various improvements were 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...
+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.
 
-É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.
+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.
 
-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 automation 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.
+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.
 
-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|.
+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.
 
-Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and Julien
-Forest acted as maintainers of features they implemented in previous
-versions of |Coq|.
+|Coq| Enhancement Proposals (CEPs for short) and open pull request discussions
+were used to discuss publicly the new features.
 
-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
-Kaliszyk, 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.
+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.
 
-| Palaiseau, June 2008
-| Hugo Herbelin
+| Paris, August 2017,
+| Matthieu Sozeau and the |Coq| development team
 |
 
-Version 8.3
+Version 8.6
 -----------
 
-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 typeclasses 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 platform 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
-|
-
-Version 8.4
------------
+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:
 
-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.
+-  A new, faster state-of-the-art universe constraint checker, by
+   Jacques-Henri Jourdan.
 
-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, ...
+-  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.
 
-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 Pierre Letouzey
-to reimplement info and Show Script differently.
+-  More access to the proof engine features from Ltac: goal management
+   primitives, range selectors and a :tacn:`typeclasses eauto` engine handling
+   multiple goals and multiple successes, by Cyprien Mangin, Matthieu
+   Sozeau and Arnaud Spiwack.
 
-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|.
+-  Tactic behavior uniformization and specification, generalization of
+   intro-patterns by Hugo Herbelin and others.
 
-Coq 8.4 also comes with a bunch of various smaller-scale changes
-and improvements regarding the different components of the system.
+-  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.
 
-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|.
+-  Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
 
-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).
+-  The ssreflect subterm selection algorithm by Georges Gonthier and
+   Enrico Tassi is now accessible to tactic writers through the
+   ssrmatching plugin.
 
-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.
+-  Integration of LtacProf, a profiler for Ltac by Jason Gross, Paul
+   Steckler, Enrico Tassi and Tobias Tebbi.
 
-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
-typeclass 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.
+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.
 
-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 :tacn:`constr_eq`, :tacn:`is_evar`, and :tacn:`has_evar`, to be used
-when writing complex tactics. Enrico Tassi added support to fine-tuning
-the behavior of :tacn:`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
-:tacn:`vm_compute`. Bug fixes and miscellaneous improvements of the tactic
-language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau.
+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).
 
-Regarding decision tactics, Loïc Pottier maintained nsatz, moving in
-particular to a typeclass based reification of goals while Frédéric
-Besson maintained Micromega, adding in particular support for division.
+Maxime Dénès maintained the native compilation machinery.
 
-Regarding vernacular commands, Stéphane Glondu provided new commands to
-analyze the structure of type universes.
+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.
 
-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`.
+In patterns and terms, @, abbreviations and notations are now
+interpreted the same way, by Hugo Herbelin.
 
-Pierre Corbineau maintained the Mathematical Proof Language (C-zar).
+Name handling for universes has been improved by Pierre-Marie Pédrot and
+Matthieu Sozeau. The minimization algorithm has been improved by
+Matthieu Sozeau.
 
-Bruno Barras and Benjamin Grégoire maintained the call-by-value
-reduction machines.
+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 extraction mechanism benefited from several improvements provided by
-Pierre Letouzey.
+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.
 
-Pierre Letouzey maintained the module system, with contributions from
-Élie Soubiran.
+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.
 
-Julien Forest maintained the Function command.
+Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre
+Letouzey and others.
 
-Matthieu Sozeau maintained the setoid rewriting mechanism.
+Emilio Jesús Gallego Arias contributed many cleanups and refactorings of
+the pretty-printing and user interface communication components.
 
-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.
+Frédéric Besson maintained the micromega tactic.
 
-Bruno Barras and Pierre Letouzey maintained the `coqchk` checker.
+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/.
 
-Pierre Courtieu and Arnaud Spiwack contributed new features for using
-Coq through Proof General.
+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.
 
-The Dp plugin has been removed. Use the plugin provided with Why 3
-instead (http://why3.lri.fr/).
+Matej Košík maintained and greatly improved the continuous integration
+setup and the testing of |Coq| contributions. He also contributed many API
+improvements and code cleanups throughout the system.
 
-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.
+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 Košík, 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.
 
-A new backtracking mechanism simplifying the task of external interfaces
-has been designed by Pierre Letouzey.
+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.
 
-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.
+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.
 
-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.
+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.
 
-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.
+Started during this period, an effort is led by Yves Bertot and Maxime
+Dénès to put together a |Coq| consortium.
 
-| Paris, December 2011
-| Hugo Herbelin
+| Paris, November 2016,
+| Matthieu Sozeau and the |Coq| development team
 |
 
 Version 8.5
@@ -1383,502 +656,507 @@ Tankink. Maxime Dénès coordinated the release process.
 | Hugo Herbelin, Matthieu Sozeau and the |Coq| development team
 |
 
-Version 8.6
+Version 8.4
 -----------
 
-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.
+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.
 
--  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.
+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, ...
 
--  More access to the proof engine features from Ltac: goal management
-   primitives, range selectors and a :tacn:`typeclasses eauto` engine handling
-   multiple goals and multiple successes, by Cyprien Mangin, Matthieu
-   Sozeau and Arnaud Spiwack.
+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 Pierre Letouzey
+to reimplement info and Show Script differently.
 
--  Tactic behavior uniformization and specification, generalization of
-   intro-patterns by Hugo Herbelin and others.
+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|.
 
--  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.
+Coq 8.4 also comes with a bunch of various smaller-scale changes
+and improvements regarding the different components of the system.
 
--  Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
+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 ssreflect subterm selection algorithm by Georges Gonthier and
-   Enrico Tassi is now accessible to tactic writers through the
-   ssrmatching plugin.
+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).
 
--  Integration of LtacProf, a profiler for Ltac by Jason Gross, Paul
-   Steckler, Enrico Tassi and Tobias Tebbi.
+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.
 
-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.
+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
+typeclass 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.
 
-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).
+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 :tacn:`constr_eq`, :tacn:`is_evar`, and :tacn:`has_evar`, to be used
+when writing complex tactics. Enrico Tassi added support to fine-tuning
+the behavior of :tacn:`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
+:tacn:`vm_compute`. Bug fixes and miscellaneous improvements of the tactic
+language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau.
 
-Maxime Dénès maintained the native compilation machinery.
+Regarding decision tactics, Loïc Pottier maintained nsatz, moving in
+particular to a typeclass based reification of goals while Frédéric
+Besson maintained Micromega, adding in particular support for division.
 
-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.
+Regarding vernacular commands, Stéphane Glondu provided new commands to
+analyze the structure of type universes.
 
-In patterns and terms, @, abbreviations and notations are now
-interpreted the same way, by Hugo Herbelin.
+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`.
 
-Name handling for universes has been improved by Pierre-Marie Pédrot and
-Matthieu Sozeau. The minimization algorithm has been improved by
-Matthieu Sozeau.
+Pierre Corbineau maintained the Mathematical Proof Language (C-zar).
 
-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.
+Bruno Barras and Benjamin Grégoire maintained the call-by-value
+reduction machines.
 
-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 extraction mechanism benefited from several improvements provided by
+Pierre Letouzey.
 
-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.
+Pierre Letouzey maintained the module system, with contributions from
+Élie Soubiran.
 
-Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre
-Letouzey and others.
+Julien Forest maintained the Function command.
 
-Emilio Jesús Gallego Arias contributed many cleanups and refactorings of
-the pretty-printing and user interface communication components.
+Matthieu Sozeau maintained the setoid rewriting mechanism.
 
-Frédéric Besson maintained the micromega tactic.
+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.
 
-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/.
+Bruno Barras and Pierre Letouzey maintained the `coqchk` checker.
 
-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.
+Pierre Courtieu and Arnaud Spiwack contributed new features for using
+Coq through Proof General.
 
-Matej Košík maintained and greatly improved the continuous integration
-setup and the testing of |Coq| contributions. He also contributed many API
-improvements and code cleanups throughout the system.
+The Dp plugin has been removed. Use the plugin provided with Why 3
+instead (http://why3.lri.fr/).
 
-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 Košík, 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.
+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.
 
-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.
+A new backtracking mechanism simplifying the task of external interfaces
+has been designed by Pierre Letouzey.
 
-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.
+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.
 
-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.
+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.
 
-Started during this period, an effort is led by Yves Bertot and Maxime
-Dénès to put together a |Coq| consortium.
+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, November 2016,
-| Matthieu Sozeau and the |Coq| development team
+| Paris, December 2011
+| Hugo Herbelin
 |
 
-Version 8.7
+Version 8.3
 -----------
 
-|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:
+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.
 
-- New tactics: variants of tactics supporting existential variables :tacn:`eassert`,
-  :tacn:`eenough`, etc... by Hugo Herbelin. Tactics ``extensionality in H`` and
-  :tacn:`inversion_sigma` by Jason Gross, ``specialize with ...`` accepting partial bindings
-  by Pierre Courtieu.
+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}`.
 
-- ``Cumulative Polymorphic Inductive`` types, allowing cumulativity of universes to
-  go through applied inductive types, by Amin Timany and Matthieu Sozeau.
+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.
 
-- Integration of the SSReflect plugin and its documentation in the reference
-  manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès.
+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 ``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.
+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.
 
-|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.
+Matthieu Sozeau extended and refined the typeclasses 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 platform 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.
 
-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.
+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.
 
-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.
+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, ...
 
-Thomas Sibut-Pinote and Hugo Herbelin added support for side effect hooks in
-cbv, cbn and simpl. The side effects are provided via a plugin available at
-https://github.com/herbelin/reduction-effects/.
+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.
 
-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.
+| Paris, April 2010
+| Hugo Herbelin
+|
 
-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).
+Version 8.2
+-----------
 
-Standard library additions and improvements by Jason Gross, Pierre Letouzey and
-others, documented in the ``CHANGES.md`` file.
+Coq version 8.2 adds new features, new libraries and improves on many
+various aspects.
 
-The mathematical proof language/declarative mode plugin was removed from the
-archive.
+Regarding the language of |Coq|, the main novelty is the introduction by
+Matthieu Sozeau of a package of commands providing Haskell-style typeclasses.
+Typeclasses, which come with a few convenient features such as
+type-based resolution of implicit arguments, play a new landmark role
+in the architecture of |Coq| with respect to automation. For
+instance, thanks to typeclass support, Matthieu Sozeau could
+implement a new resolution-based version of the tactics dedicated to
+rewriting on arbitrary transitive relations.
 
-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/.
+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 arithmetic 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 automation in
+presence of various number-theory concepts.
 
-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.
+Frédéric Besson contributed a reflective 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.
 
-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.
+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 arithmetic for efficiently computing
+with the library of integers he developed.
 
-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.
+Beside the libraries, various improvements were 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...
 
-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.
+É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.
 
-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.
+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 automation 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.
 
-|Coq| Enhancement Proposals (CEPs for short) and open pull request discussions
-were used to discuss publicly the new features.
+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|.
 
-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.
+Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and Julien
+Forest acted as maintainers of features they implemented in previous
+versions of |Coq|.
 
-| Paris, August 2017,
-| Matthieu Sozeau and the |Coq| development team
+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
+Kaliszyk, 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
 |
 
-Version 8.8
+Version 8.1
 -----------
 
-|Coq| version 8.8 contains the result of refinements and stabilization of
-features and deprecations, cleanups of the internals of the system along
-with a few new features. The main user visible changes are:
+Coq version 8.1 adds various new functionalities.
 
-- Kernel: fix a subject reduction failure due to allowing fixpoints
-  on non-recursive values, by Matthieu Sozeau.
-  Handling of evars in the VM (the kernel still does not accept evars)
-  by Pierre-Marie Pédrot.
+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.
 
-- Notations: many improvements on recursive notations and support for
-  destructuring patterns in the syntax of notations by Hugo Herbelin.
+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).
 
-- Proof language: tacticals for profiling, timing and checking success
-  or failure of tactics by Jason Gross. The focusing bracket ``{``
-  supports single-numbered goal selectors, e.g. ``2:{``, by Théo
-  Zimmermann.
+Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary
+compatible equivalence relations. He also generalized rewriting to
+arbitrary transition systems.
 
-- Vernacular: deprecation of commands and more uniform handling of the
-  ``Local`` flag, by Vincent Laporte and Maxime Dénès, part of a larger
-  attribute system overhaul. Experimental ``Show Extraction`` command by
-  Pierre Letouzey. Coercion now accepts ``Prop`` or ``Type`` as a source
-  by Arthur Charguéraud. ``Export`` modifier for options allowing to
-  export the option to modules that ``Import`` and not only ``Require``
-  a module, by Pierre-Marie Pédrot.
+Claudio Sacerdoti Coen added new features to the module system.
 
-- Universes: many user-level and API level enhancements: qualified
-  naming and printing, variance annotations for cumulative inductive
-  types, more general constraints and enhancements of the minimization
-  heuristics, interaction with modules by Gaëtan Gilbert, Pierre-Marie
-  Pédrot and Matthieu Sozeau.
+Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new, more
+efficient and more general simplification algorithm for rings and
+semirings.
 
-- Library: Decimal Numbers library by Pierre Letouzey and various small
-  improvements.
+Laurent Théry and Bruno Barras developed a new, significantly more
+efficient simplification algorithm for fields.
 
-- Documentation: a large community effort resulted in the migration
-  of the reference manual to the Sphinx documentation tool. The result
-  is this manual. The new documentation infrastructure (based on Sphinx)
-  is by Clément Pit-Claudel. The migration was coordinated by Maxime Dénès
-  and Paul Steckler, with some help of Théo Zimmermann during the
-  final integration phase. The 14 people who ported the manual are
-  Calvin Beck, Heiko Becker, Yves Bertot, Maxime Dénès, Richard Ford,
-  Pierre Letouzey, Assia Mahboubi, Clément Pit-Claudel,
-  Laurence Rideau, Matthieu Sozeau, Paul Steckler, Enrico Tassi,
-  Laurent Théry, Nikita Zyuzin.
+Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
+Claudio Sacerdoti Coen added new tactic features.
 
-- Tools: experimental ``-mangle-names`` option to ``coqtop``/``coqc`` for
-  linting proof scripts, by Jasper Hugunin.
+Hugo Herbelin implemented matching on disjunctive patterns.
 
-On the implementation side, the ``dev/doc/changes.md`` file
-documents the numerous changes to the implementation and improvements of
-interfaces. The file provides guidelines on porting a plugin to the new
-version.
+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.
 
-Version 8.8 also comes with a bunch of smaller-scale changes and
-improvements regarding the different components of the system.
-Most important ones are documented in the ``CHANGES.md`` file.
+Matthieu Sozeau developed Russell, an experimental language to specify
+the behavior of programs with subtypes.
 
-The efficiency of the whole system has seen improvements thanks to
-contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and
-Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
-Steckler.
+A mechanism to automatically use some specific tactic to solve
+unresolved implicit has been implemented by Hugo Herbelin.
 
-The official wiki and the bugtracker of |Coq| migrated to the GitHub
-platform, thanks to the work of Pierre Letouzey and Théo
-Zimmermann. Gaëtan Gilbert, Emilio Jesús Gallego Arias worked on
-maintaining and improving the continuous integration system.
+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.
 
-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/.
+Pierre Corbineau extended his tactic for solving first-order statements.
+He wrote a reflection-based intuitionistic tautology solver.
 
-The 44 contributors for this version are Yves Bertot, Joachim Breitner, Tej
-Chajed, Arthur Charguéraud, Jacques-Pascal Deplaix, Maxime Dénès, Jim Fehrle,
-Julien Forest, Yannick Forster, Gaëtan Gilbert, Jason Gross, Samuel Gruetter,
-Thomas Hebb, Hugo Herbelin, Jasper Hugunin, Emilio Jesus Gallego Arias, Ralf
-Jung, Johannes Kloos, Matej Košík, Robbert Krebbers, Tony Beta Lambda, Vincent
-Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey, Farzon Lotfi, Cyprien Mangin,
-Guillaume Melquiond, Raphaël Monat, Carl Patenaude Poulin, Pierre-Marie Pédrot,
-Clément Pit-Claudel, Matthew Ryan, Matt Quinn, Sigurd Schneider, Bernhard
-Schommer, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack, Paul Steckler,
-Enrico Tassi, Anton Trunov, Martin Vassor, Vadim Zaliva and Théo Zimmermann.
+Pierre Courtieu, Julien Forest and Yves Bertot added extra support to
+reason on the inductive structure of recursively defined functions.
 
-Version 8.8 is the third release of |Coq| developed on a time-based
-development cycle. Its development spanned 6 months from the release of
-|Coq| 8.7 and was based on a public roadmap. The development process
-was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the
-release process. Théo Zimmermann is the maintainer of this release.
+Jean-Marc Notin significantly contributed to the general maintenance of
+the system. He also took care of ``coqdoc``.
 
-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@inria.fr 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 and Amin Timany.
-It would however be impossible to mention exhaustively the names
-of everybody who to some extent influenced the development.
+Pierre Castéran contributed to the documentation of (co-)inductive types
+and suggested improvements to the libraries.
 
-The |Coq| consortium, an organization directed towards users and
-supporters of the system, is now running and employs Maxime Dénès.
-The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès.
+Pierre Corbineau implemented a declarative mathematical proof language,
+usable in combination with the tactic-based style of proof.
 
-| Santiago de Chile, March 2018,
-| Matthieu Sozeau for the |Coq| development team
+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
 |
 
-Version 8.9
+Version 8.0
 -----------
 
-|Coq| version 8.9 contains the result of refinements and stabilization
-of features and deprecations or removals of deprecated features,
-cleanups of the internals of the system and API along with a few new
-features. This release includes many user-visible changes, including
-deprecations that are documented in ``CHANGES.md`` and new features that
-are documented in the reference manual. Here are the most important
-changes:
-
-- Kernel: mutually recursive records are now supported, by Pierre-Marie
-  Pédrot.
-
-- Notations:
-
-  - Support for autonomous grammars of terms called “custom entries”, by
-    Hugo Herbelin (see Section :ref:`custom-entries` of the reference
-    manual).
-
-  - Deprecated notations of the standard library will be removed in the
-    next version of |Coq|, see the ``CHANGES.md`` file for a script to
-    ease porting, by Jason Gross and Jean-Christophe Léchenet.
-
-  - Added the :cmd:`Numeral Notation` command for registering decimal
-    numeral notations for custom types, by Daniel de Rauglaudre, Pierre
-    Letouzey and Jason Gross.
-
-- Tactics: Introduction tactics :tacn:`intro`/:tacn:`intros` on a goal that is an
-  existential variable now force a refinement of the goal into a
-  dependent product rather than failing, by Hugo Herbelin.
-
-- Decision procedures: deprecation of tactic ``romega`` in favor of
-  :tacn:`lia` and removal of ``fourier``, replaced by :tacn:`lra` which
-  subsumes it, by Frédéric Besson, Maxime Dénès, Vincent Laporte and
-  Laurent Théry.
-
-- Proof language: focusing bracket ``{`` now supports named
-  :ref:`goals <curly-braces>`, e.g. ``[x]:{`` will focus
-  on a goal (existential variable) named ``x``, by Théo Zimmermann.
-
-- SSReflect: the implementation of delayed clear was simplified by
-  Enrico Tassi: the variables are always renamed using inaccessible
-  names when the clear switch is processed and finally cleared at the
-  end of the intro pattern. In addition to that, the use-and-discard flag
-  ``{}`` typical of rewrite rules can now be also applied to views,
-  e.g. ``=> {}/v`` applies ``v`` and then clears ``v``. See Section
-  :ref:`introduction_ssr`.
-
-- Vernacular:
+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.
 
-  - Experimental support for :ref:`attributes <gallina-attributes>` on
-    commands, by Vincent Laporte, as in ``#[local] Lemma foo : bar.``
-    Tactics and tactic notations now support the ``deprecated``
-    attribute.
+Secondly, the concrete syntax of terms has been completely revised. The
+main motivations were
 
-  - Removed deprecated commands ``Arguments Scope`` and ``Implicit
-    Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper
-    Hugunin.
+-  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 are no longer mandatory for function
+   application.
 
-  - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to
-    avoid repeating uniform parameters in constructor declarations.
+-  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.
 
-  - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by
-    Matthieu Sozeau, for controlling the opacity status of variables and
-    constants in hint databases. It is recommended to always use these
-    commands after creating a hint databse with :cmd:`Create HintDb`.
+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.
 
-  - Multiple sections with the same name are now allowed, by Jasper
-    Hugunin.
+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.
 
-- Library: additions and changes in the ``VectorDef``, ``Ascii``, and
-  ``String`` libraries. Syntax notations are now available only when using
-  ``Import`` of libraries and not merely ``Require``, by various
-  contributors (source of incompatibility, see ``CHANGES.md`` for details).
+Thirdly, a restructuring and uniformization 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.
 
-- Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof
-  steps in color, using the :opt:`Diffs` option, by Jim Fehrle.
+The fourth point is the release of |CoqIDE|, a new graphical gtk2-based
+interface fully integrated with |Coq|. Close in style to 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|.
 
-- Documentation: we integrated a large number of fixes to the new Sphinx
-  documentation by various contributors, coordinated by Clément
-  Pit-Claudel and Théo Zimmermann.
+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.
 
-- Tools: removed the ``gallina`` utility and the homebrewed ``Emacs`` mode.
+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.
 
-- Packaging: as in |Coq| 8.8.2, the Windows installer now includes many
-  more external packages that can be individually selected for
-  installation, by Michael Soegtrop.
+Bruno Barras and Hugo Herbelin have been the main contributors of the
+reflection 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.
 
-Version 8.9 also comes with a bunch of smaller-scale changes and
-improvements regarding the different components of the system.  Most
-important ones are documented in the ``CHANGES.md`` file.
+Hugo Herbelin is the main designer and implementer of the notion of
+interpretation scopes and of the commands for easily adding new
+notations.
 
-On the implementation side, the ``dev/doc/changes.md`` file documents
-the numerous changes to the implementation and improvements of
-interfaces. The file provides guidelines on porting a plugin to the new
-version and a plugin development tutorial kept in sync with Coq was
-introduced by Yves Bertot http://github.com/ybertot/plugin_tutorials.
-The new ``dev/doc/critical-bugs`` file documents the known critical bugs
-of |Coq| and affected releases.
+Hugo Herbelin is the main implementer of the restructured standard library.
 
-The efficiency of the whole system has seen improvements thanks to
-contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès.
+Pierre Corbineau is the main designer and implementer 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.
 
-Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
-Soegtrop, Théo Zimmermann worked on maintaining and improving the
-continuous integration system.
+Benjamin Monate is the developer of the |CoqIDE| graphical interface with
+contributions by Jean-Christophe Filliâtre, Pierre Letouzey, Claude
+Marché and Bruno Barras.
 
-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/.
+Claude Marché coordinated the edition of the Reference Manual for |Coq|
+V8.0.
 
-The 54 contributors for this version are Léo Andrès, Rin Arakaki,
-Benjamin Barenblat, Langston Barrett, Siddharth Bhat, Martin Bodin,
-Simon Boulier, Timothy Bourke, Joachim Breitner, Tej Chajed, Arthur
-Charguéraud, Pierre Courtieu, Maxime Dénès, Andres Erbsen, Jim Fehrle,
-Julien Forest, Emilio Jesus Gallego Arias, Gaëtan Gilbert, Matěj
-Grabovský, Jason Gross, Samuel Gruetter, Armaël Guéneau, Hugo Herbelin,
-Jasper Hugunin, Ralf Jung, Sam Pablo Kuper, Ambroise Lafont, Leonidas
-Lampropoulos, Vincent Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey,
-Jean-Christophe Léchenet, Nick Lewycky, Yishuai Li, Sven M. Hallberg,
-Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Perry E. Metzger,
-Clément Pit-Claudel, Pierre-Marie Pédrot, Daniel R. Grayson, Kazuhiko
-Sakaguchi, Michael Soegtrop, Matthieu Sozeau, Paul Steckler, Enrico
-Tassi, Laurent Théry, Anton Trunov, whitequark, Théo Winterhalter,
-Zeimer, Beta Ziliani, Théo Zimmermann.
+Pierre Letouzey and Jacek Chrząszcz respectively maintained the
+extraction tool and module system of |Coq|.
 
-Many power users helped to improve the design of the new features via
-the issue and pull request system, the |Coq| development mailing list or
-the coq-club@inria.fr mailing list. It would be impossible to mention
-exhaustively the names of everybody who to some extent influenced the
-development.
+Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other
+contributors from Sophia-Antipolis and Nijmegen participated in
+extending the library.
 
-Version 8.9 is the fourth release of |Coq| developed on a time-based
-development cycle. Its development spanned 7 months from the release of
-|Coq| 8.8. The development moved to a decentralized merging process
-during this cycle. Guillaume Melquiond was in charge of the release
-process and is the maintainer of this release. This release is the
-result of ~2,000 commits and ~500 PRs merged, closing 75+ issues.
+Julien Narboux built a NSIS-based automatic |Coq| installation tool for
+the Windows platform.
 
-The |Coq| development team welcomed Vincent Laporte, a new |Coq|
-engineer working with Maxime Dénès in the |Coq| consortium.
+Hugo Herbelin and Christine Paulin coordinated the development which was
+under the responsibility of Christine Paulin.
 
-| Paris, November 2018,
-| Matthieu Sozeau for the |Coq| development team
+| Palaiseau & Orsay, Apr. 2004
+| Hugo Herbelin & Christine Paulin
+| (updated Apr. 2006)
 |
diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst
new file mode 100644
index 0000000000..e0b5e5ca9a
--- /dev/null
+++ b/doc/sphinx/history.rst
@@ -0,0 +1,725 @@
+--------------------
+Early history of Coq
+--------------------
+
+Historical roots
+----------------
+
+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 [#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
+λ-calculus occurred with Church’s *Simple Theory of
+Types*. The λ-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 λ-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 language, 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 semidecision 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.
+
+.. [#years] At the time of writting, i.e. 1995.
+
+Brief summary of the versions up to 5.10
+----------------------------------------
+
+.. note::
+   This summary was written in 1995 together with the previous
+   section and formed the initial version of the Credits chapter
+   (that has since then been appended to, at each new release).
+   A more comprehensive description of these early versions is
+   available in the next few sections, which were written in 2015.
+
+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
+λ-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
+λ-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-ends. 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
+|
+
+Version 1
+---------
+
+.. note::
+
+   These additional notes come from a document written
+   in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin
+   to accompany their public release of the archive of versions 1.10 to 6.2
+   of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and
+   implemented in the Formel team, joint between the INRIA Rocquencourt
+   laboratory and the Ecole Normale Supérieure of Paris, from 1984
+   onwards.
+
+This software is a prototype type-checker for a higher-order logical
+formalism known as the Theory of Constructions, presented in his PhD
+thesis by Thierry Coquand, with influences from Girard's system F and
+de Bruijn's Automath.  The metamathematical analysis of the system is
+the PhD work of Thierry Coquand. The software is mostly the work of
+Gérard Huet.  Most of the mathematical examples verified with the
+software are due to Thierry Coquand.
+
+The programming language of the CONSTR software (as it was called at
+the time) was a version of ML adapted from the Edinburgh LCF system
+and running on a LISP backend. The main improvements from the original
+LCF ML were that ML was compiled rather than interpreted (Gérard Huet
+building on the original translator by Lockwood Morris), and that it
+was enriched by recursively defined types (work of Guy
+Cousineau). This ancestor of CAML was used and improved by Larry
+Paulson for his implementation of Cambridge LCF.
+
+Software developments of this prototype occurred from late 1983 to
+early 1985.
+
+Version 1.10 was frozen on December 22nd 1984. It is the version used
+for the examples in Thierry Coquand's thesis, defended on January 31st
+1985. There was a unique binding operator, used both for universal
+quantification (dependent product) at the level of types and
+functional abstraction (λ) at the level of terms/proofs, in the manner
+of Automath. Substitution (λ-reduction) was implemented using de
+Bruijn's indexes.
+
+Version 1.11 was frozen on February 19th, 1985. It is the version used
+for the examples in the paper: T. Coquand, G. Huet. *Constructions: A
+Higher Order Proof System for Mechanizing Mathematics* :cite:`CH85`.
+
+Christine Paulin joined the team at this point, for her DEA research
+internship.  In her DEA memoir (August 1985) she presents developments
+for the *lambo* function – :math:`\text{lambo}(f)(n)` computes the minimal
+:math:`m` such that :math:`f(m)` is greater than :math:`n`, for :math:`f`
+an increasing integer function, a challenge for constructive mathematics.
+She also encoded the majority voting algorithm of Boyer and Moore.
+
+Version 2
+---------
+
+The formal system, now renamed as the *Calculus of Constructions*, was
+presented with a proof of consistency and comparisons with proof
+systems of Per Martin Löf, Girard, and the Automath family of N. de
+Bruijn, in the paper: T. Coquand and G. Huet. *The Calculus of
+Constructions* :cite:`CH88`.
+
+An abstraction of the software design, in the form of an abstract
+machine for proof checking, and a fuller sequence of mathematical
+developments was presented in: T. Coquand, G. Huet. *Concepts
+Mathématiques et Informatiques Formalisés dans le Calcul des
+Constructions* :cite:`CH87`.
+
+Version 2.8 was frozen on December 16th, 1985, and served for
+developing the examples in the above papers.
+
+This calculus was then enriched in version 2.9 with a cumulative
+hierarchy of universes. Universe levels were initially explicit
+natural numbers.  Another improvement was the possibility of automatic
+synthesis of implicit type arguments, relieving the user of tedious
+redundant declarations.
+
+Christine Paulin wrote an article *Algorithm development in the
+Calculus of Constructions* :cite:`P86`. Besides *lambo* and *majority*,
+she presents *quicksort* and a text formatting algorithm.
+
+Version 2.13 of the Calculus of Constructions with universes was
+frozen on June 25th, 1986.
+
+A synthetic presentation of type theory along constructive lines with
+ML algorithms was given by Gérard Huet in his May 1986 CMU course
+notes *Formal Structures for Computation and Deduction*. Its chapter
+*Induction and Recursion in the Theory of Constructions* was presented
+as an invited paper at the Joint Conference on Theory and Practice of
+Software Development TAPSOFT’87 at Pise in March 1987, and published
+as *Induction Principles Formalized in the Calculus of
+Constructions* :cite:`H88`.
+
+Version 3
+---------
+
+This version saw the beginning of proof automation, with a search
+algorithm inspired from PROLOG and the applicative logic programming
+programs of the course notes *Formal structures for computation and
+deduction*.  The search algorithm was implemented in ML by Thierry
+Coquand.  The proof system could thus be used in two modes: proof
+verification and proof synthesis, with tactics such as ``AUTO``.
+
+The implementation language was now called CAML, for Categorical
+Abstract Machine Language. It used as backend the LLM3 virtual machine
+of Le Lisp by Jérôme Chailloux. The main developers of CAML were
+Michel Mauny, Ascander Suarez and Pierre Weis.
+
+V3.1 was started in the summer of 1986, V3.2 was frozen at the end of
+November 1986. V3.4 was developed in the first half of 1987.
+
+Thierry Coquand held a post-doctoral position in Cambrige University
+in 1986-87, where he developed a variant implementation in SML, with
+which he wrote some developments on fixpoints in Scott's domains.
+
+Version 4
+---------
+
+This version saw the beginning of program extraction from proofs, with
+two varieties of the type ``Prop`` of propositions, indicating
+constructive intent.  The proof extraction algorithms were implemented
+by Christine Paulin-Mohring.
+
+V4.1 was frozen on July 24th, 1987. It had a first identified library
+of mathematical developments (directory ``exemples``), with libraries
+``Logic`` (containing impredicative encodings of intuitionistic logic and
+algebraic primitives for booleans, natural numbers and list), ``Peano``
+developing second-order Peano arithmetic, ``Arith`` defining addition,
+multiplication, euclidean division and factorial. Typical developments
+were the Knaster-Tarski theorem and Newman's lemma from rewriting
+theory.
+
+V4.2 was a joint development of a team consisting of Thierry Coquand,
+Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the
+log of changes.  It was frozen on September 1987 as the last version
+implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable
+development system.
+
+V4.3 saw the first top-level of the system. Instead of evaluating
+explicit quotations, the user could develop his mathematics in a
+high-level language called the mathematical vernacular (following
+Automath terminology).  The user could develop files in the vernacular
+notation (with ``.v`` extension) which were now separate from the ``ml``
+sources of the implementation.  Gilles Dowek joined the team to
+develop the vernacular language as his DEA internship research.
+
+A notion of sticky constant was introduced, in order to keep names of
+lemmas when local hypotheses of proofs were discharged. This gave a
+notion of global mathematical environment with local sections.
+
+Another significant practical change was that the system, originally
+developped on the VAX central computer of our lab, was transferred on
+SUN personal workstations, allowing a level of distributed
+development.  The extraction algorithm was modified, with three
+annotations ``Pos``, ``Null`` and ``Typ`` decorating the sorts ``Prop``
+and ``Type``.
+
+Version 4.3 was frozen at the end of November 1987, and was
+distributed to an early community of users (among those were Hugo
+Herbelin and Loic Colson).
+
+V4.4 saw the first version of (encoded) inductive types.  Now natural
+numbers could be defined as::
+
+  [source, coq]
+  Inductive NAT : Prop = O : NAT | Succ : NAT->NAT.
+
+These inductive types were encoded impredicatively in the calculus,
+using a subsystem *rec* due to Christine Paulin.  V4.4 was frozen on
+March 6th 1988.
+
+Version 4.5 was the first one to support inductive types and program
+extraction.  Its banner was *Calcul des Constructions avec
+Réalisations et Synthèse*.  The vernacular language was enriched to
+accommodate extraction commands.
+
+The verification engine design was presented as: G. Huet. *The
+Constructive Engine*. Version 4.5. Invited Conference, 2nd European
+Symposium on Programming, Nancy, March 88.  The final paper,
+describing the V4.9 implementation, appeared in: A perspective in
+Theoretical Computer Science, Commemorative Volume in memory of Gift
+Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.
+
+Version 4.5 was demonstrated in June 1988 at the YoP Institute on
+Logical Foundations of Functional Programming organized by Gérard Huet
+at Austin, Texas.
+
+Version 4.6 was started during the summer of 1988. Its main
+improvement was the complete rehaul of the proof synthesis engine by
+Thierry Coquand, with a tree structure of goals.
+
+Its source code was communicated to Randy Pollack on September 2nd
+1988.  It evolved progressively into LEGO, proof system for Luo's
+formalism of Extended Calculus of Constructions.
+
+The discharge tactic was modified by Gérard Huet to allow for
+inter-dependencies in discharged lemmas. Christine Paulin improved the
+inductive definition scheme in order to accommodate predicates of any
+arity.
+
+Version 4.7 was started on September 6th, 1988.
+
+This version starts exploiting the CAML notion of module in order to
+improve the modularity of the implementation. Now the term verifier is
+identified as a proper module Machine, which the structure of its
+internal data structures being hidden and thus accessible only through
+the legitimate operations.  This machine (the constructive engine) was
+the trusted core of the implementation. The proof synthesis mechanism
+was a separate proof term generator. Once a complete proof term was
+synthesized with the help of tactics, it was entirely re-checked by
+the engine. Thus there was no need to certify the tactics, and the
+system took advantage of this fact by having tactics ignore the
+universe levels, universe consistency check being relegated to the
+final type-checking pass. This induced a certain puzzlement in early
+users who saw, after a successful proof search, their ``QED`` followed
+by silence, followed by a failure message due to a universe
+inconsistency…
+
+The set of examples comprise set theory experiments by Hugo Herbelin,
+and notably the Schroeder-Bernstein theorem.
+
+Version 4.8, started on October 8th, 1988, saw a major
+re-implementation of the abstract syntax type ``constr``, separating
+variables of the formalism and metavariables denoting incomplete terms
+managed by the search mechanism.  A notion of level (with three values
+``TYPE``, ``OBJECT`` and ``PROOF``) is made explicit and a type judgement
+clarifies the constructions, whose implementation is now fully
+explicit. Structural equality is speeded up by using pointer equality,
+yielding spectacular improvements. Thierry Coquand adapts the proof
+synthesis to the new representation, and simplifies pattern matching
+to first-order predicate calculus matching, with important performance
+gain.
+
+A new representation of the universe hierarchy is then defined by
+Gérard Huet.  Universe levels are now implemented implicitly, through
+a hidden graph of abstract levels constrained with an order relation.
+Checking acyclicity of the graph insures well-foundedness of the
+ordering, and thus consistency. This was documented in a memo *Adding
+Type:Type to the Calculus of Constructions* which was never published.
+
+The development version is released as a stable 4.8 at the end of
+1988.
+
+Version 4.9 is released on March 1st 1989, with the new "elastic"
+universe hierarchy.
+
+The spring of 1989 saw the first attempt at documenting the system
+usage, with a number of papers describing the formalism:
+
+- *Metamathematical Investigations of a Calculus of Constructions*, by
+  Thierry Coquand :cite:`C90`,
+
+- *Inductive definitions in the Calculus of Constructions*, by
+  Christine Paulin-Mohrin,
+
+- *Extracting Fω's programs from proofs in the Calculus of
+  Constructions*, by Christine Paulin-Mohring* :cite:`P89`,
+
+- *The Constructive Engine*, by Gérard Huet :cite:`H89`,
+
+as well as a number of user guides:
+
+- *A short user's guide for the Constructions*, Version 4.10, by Gérard Huet
+- *A Vernacular Syllabus*, by Gilles Dowek.
+- *The Tactics Theorem Prover, User's guide*, Version 4.10, by Thierry
+  Coquand.
+
+Stable V4.10, released on May 1st, 1989, was then a mature system,
+distributed with CAML V2.6.
+
+In the mean time, Thierry Coquand and Christine Paulin-Mohring had
+been investigating how to add native inductive types to the Calculus
+of Constructions, in the manner of Per Martin-Löf's Intuitionistic
+Type Theory. The impredicative encoding had already been presented in:
+F. Pfenning and C. Paulin-Mohring. *Inductively defined types in the
+Calculus of Constructions* :cite:`PP90`. An extension of the calculus
+with primitive inductive types appeared in: T. Coquand and
+C. Paulin-Mohring. *Inductively defined types* :cite:`CP90`.
+
+This led to the Calculus of Inductive Constructions, logical formalism
+implemented in Versions 5 upward of the system, and documented in:
+C. Paulin-Mohring. *Inductive Definitions in the System Coq - Rules
+and Properties* :cite:`P93`.
+
+The last version of CONSTR is Version 4.11, which was last distributed
+in the spring of 1990. It was demonstrated at the first workshop of
+the European Basic Research Action Logical Frameworks In Sophia
+Antipolis in May 1990.
+
+Version 5
+---------
+
+At the end of 1989, Version 5.1 was started, and renamed as the system
+Coq for the Calculus of Inductive Constructions. It was then ported to
+the new stand-alone implementation of ML called Caml-light.
+
+In 1990 many changes occurred. Thierry Coquand left for Chalmers
+University in Göteborg. Christine Paulin-Mohring took a CNRS
+researcher position at the LIP laboratory of École Normale Supérieure
+de Lyon. Project Formel was terminated, and gave rise to two teams:
+Cristal at INRIA-Roquencourt, that continued developments in
+functional programming with Caml-light then OCaml, and Coq, continuing
+the type theory research, with a joint team headed by Gérard Huet at
+INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory
+of CNRS-ENS Lyon.
+
+Chetan Murthy joined the team in 1991 and became the main software
+architect of Version 5. He completely rehauled the implementation for
+efficiency.  Versions 5.6 and 5.8 were major distributed versions,
+with complete documentation and a library of users' developements. The
+use of the RCS revision control system, and systematic ChangeLog
+files, allow a more precise tracking of the software developments.
+
+| September 2015 +
+| Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.
+|
+
+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
+|
+
+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 reduction 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 the 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
+|
+
+Version 6.3
+-----------
+
+The main changes in version V6.3 were 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 fixed 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
+|
+
+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 efficiency of the reduction algorithm 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, reflection-based version of the Omega
+decision procedure.
+
+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 Chrząszcz 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
+|
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index 5a349fcf75..a91c6a9c5f 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -23,7 +23,8 @@ Contents
    :caption: Preamble
 
    self
-   credits
+   history
+   changes
 
 .. toctree::
    :caption: The language
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index ff3971aee4..708820fff7 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -15,7 +15,9 @@ Introduction
    Company-Coq :cite:`Pit16`
    (see https://github.com/cpitclaudel/company-coq).
 
-.. include:: credits.rst
+.. include:: history.rst
+
+.. include:: changes.rst
 
 ------------
 The language