path: root/doc/refman/RefMan-pre.tex

%BEGIN LATEX
\setheaders{Credits}
%END LATEX
\chapter*{Credits}
%\addcontentsline{toc}{section}{Credits}

\Coq{}~ is a proof assistant for higher-order logic, allowing the
development of computer programs consistent with their formal
specification.  It is the result of about ten years of research of the
Coq project.  We shall briefly survey here three main aspects: the
\emph{logical language} in which we write our axiomatizations and
specifications, the \emph{proof assistant} which allows the development
of verified mathematical proofs, and the \emph{program extractor} which
synthesizes computer programs obeying their formal specifications,
written as logical assertions in the language.

The logical language used by {\Coq} is a variety of type theory,
called the \emph{Calculus of Inductive Constructions}. Without going
back to Leibniz and Boole, we can date the creation of what is now
called mathematical logic to the work of Frege and Peano at the turn
of the century. The discovery of antinomies in the free use of
predicates or comprehension principles prompted Russell to restrict
predicate calculus with a stratification of \emph{types}. This effort
culminated with \emph{Principia Mathematica}, the first systematic
attempt at a formal foundation of mathematics.  A simplification of
this system along the lines of simply typed $\lambda$-calculus
occurred with Church's \emph{Simple Theory of Types}.  The
$\lambda$-calculus notation, originally used for expressing
functionality, could also be used as an encoding of natural deduction
proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the
\emph{Automath} project, the first full-scale attempt to develop and
mechanically verify mathematical proofs. This effort culminated with
Jutting's verification of Landau's \emph{Grundlagen} in the 1970's.
Exploiting this Curry-Howard isomorphism, notable achievements in
proof theory saw the emergence of two type-theoretic frameworks; the
first one, Martin-L\"of's \emph{Intuitionistic Theory of Types},
attempts a new foundation of mathematics on constructive principles.
The second one, Girard's polymorphic $\lambda$-calculus $F_\omega$, is
a very strong functional system in which we may represent higher-order
logic proof structures.  Combining both systems in a higher-order
extension of the Automath languages, T. Coquand presented in 1985 the
first version of the \emph{Calculus of Constructions}, CoC. This strong
logical system allowed powerful axiomatizations, but direct inductive
definitions were not possible, and inductive notions had to be defined
indirectly through functional encodings, which introduced
inefficiencies and awkwardness. The formalism was extended in 1989 by
T. Coquand and C. Paulin with primitive inductive definitions, leading
to the current \emph{Calculus of Inductive Constructions}.  This
extended formalism is not rigorously defined here. Rather, numerous
concrete examples are discussed. We refer the interested reader to
relevant research papers for more information about the formalism, its
meta-theoretic properties, and semantics. However, it should not be
necessary to understand this theoretical material in order to write
specifications. It is possible to understand the Calculus of Inductive
Constructions at a higher level, as a mixture of predicate calculus,
inductive predicate definitions presented as typed PROLOG, and
recursive function definitions close to the language ML.

Automated theorem-proving was pioneered in the 1960's by Davis and
Putnam in propositional calculus.  A complete mechanization (in the
sense of a semi-decision procedure) of classical first-order logic was
proposed in 1965 by J.A. Robinson, with a single uniform inference
rule called \emph{resolution}. Resolution relies on solving equations
in free algebras (i.e. term structures), using the \emph{unification
  algorithm}. Many refinements of resolution were studied in the
1970's, but few convincing implementations were realized, except of
course that PROLOG is in some sense issued from this effort.  A less
ambitious approach to proof development is computer-aided
proof-checking.  The most notable proof-checkers developed in the
1970's were LCF, designed by R. Milner and his colleagues at U.
Edinburgh, specialized in proving properties about denotational
semantics recursion equations, and the Boyer and Moore theorem-prover,
an automation of primitive recursion over inductive data types. While
the Boyer-Moore theorem-prover attempted to synthesize proofs by a
combination of automated methods, LCF constructed its proofs through
the programming of \emph{tactics}, written in a high-level functional
meta-language, ML.

The salient feature which clearly distinguishes our proof assistant
from say LCF or Boyer and Moore's, is its possibility to extract
programs from the constructive contents of proofs. This computational
interpretation of proof objects, in the tradition of Bishop's
constructive mathematics, is based on a realizability interpretation,
in the sense of Kleene, due to C.  Paulin. The user must just mark his
intention by separating in the logical statements the assertions
stating the existence of a computational object from the logical
assertions which specify its properties, but which may be considered
as just comments in the corresponding program. Given this information,
the system automatically extracts a functional term from a consistency
proof of its specifications.  This functional term may be in turn
compiled into an actual computer program.  This methodology of
extracting programs from proofs is a revolutionary paradigm for
software engineering.  Program synthesis has long been a theme of
research in artificial intelligence, pioneered by R. Waldinger. The
Tablog system of Z. Manna and R. Waldinger allows the deductive
synthesis of functional programs from proofs in tableau form of their
specifications, written in a variety of first-order logic. Development
of a systematic \emph{programming logic}, based on extensions of
Martin-L\"of's type theory, was undertaken at Cornell U. by the Nuprl
team, headed by R. Constable.  The first actual program extractor, PX,
was designed and implemented around 1985 by S. Hayashi from Kyoto
University.  It allows the extraction of a LISP program from a proof
in a logical system inspired by the logical formalisms of S. Feferman.
Interest in this methodology is growing in the theoretical computer
science community. We can foresee the day when actual computer systems
used in applications will contain certified modules, automatically
generated from a consistency proof of their formal specifications. We
are however still far from being able to use this methodology in a
smooth interaction with the standard tools from software engineering,
i.e. compilers, linkers, run-time systems taking advantage of special
hardware, debuggers, and the like. We hope that {\Coq} can be of use
to researchers interested in experimenting with this new methodology.

A first implementation of CoC was started in 1984 by G. Huet and T.
Coquand.  Its implementation language was CAML, a functional
programming language from the ML family designed at INRIA in
Rocquencourt. The core of this system was a proof-checker for CoC seen
as a typed $\lambda$-calculus, called the \emph{Constructive Engine}.
This engine was operated through a high-level notation permitting the
declaration of axioms and parameters, the definition of mathematical
types and objects, and the explicit construction of proof objects
encoded as $\lambda$-terms. A section mechanism, designed and
implemented by G. Dowek, allowed hierarchical developments of
mathematical theories. This high-level language was called the
\emph{Mathematical Vernacular}.  Furthermore, an interactive
\emph{Theorem Prover} permitted the incremental construction of proof
trees in a top-down manner, subgoaling recursively and backtracking
from dead-alleys. The theorem prover executed tactics written in CAML,
in the LCF fashion.  A basic set of tactics was predefined, which the
user could extend by his own specific tactics. This system (Version
4.10) was released in 1989.  Then, the system was extended to deal
with the new calculus with inductive types by C. Paulin, with
corresponding new tactics for proofs by induction.  A new standard set
of tactics was streamlined, and the vernacular extended for tactics
execution. A package to compile programs extracted from proofs to
actual computer programs in CAML or some other functional language was
designed and implemented by B. Werner.  A new user-interface, relying
on a CAML-X interface by D. de Rauglaudre, was designed and
implemented by A. Felty. It allowed operation of the theorem-prover
through the manipulation of windows, menus, mouse-sensitive buttons,
and other widgets. This system (Version 5.6) was released in 1991.

\Coq{} was ported to the new implementation Caml-light of X. Leroy and
D.  Doligez by D. de Rauglaudre (Version 5.7) in 1992.  A new version
of \Coq{} was then coordinated by C. Murthy, with new tools designed
by C.  Parent to prove properties of ML programs (this methodology is
dual to program extraction) and a new user-interaction loop.  This
system (Version 5.8) was released in May 1993.  A Centaur interface
\textsc{CTCoq} was then developed by Y. Bertot from the Croap project
from INRIA-Sophia-Antipolis.

In parallel, G. Dowek and H. Herbelin developed a new proof engine,
allowing the general manipulation of existential variables
consistently with dependent types in an experimental version of \Coq{}
(V5.9).

The version V5.10 of \Coq{} is based on a generic system for
manipulating terms with binding operators due to Chet Murthy. A new
proof engine allows the parallel development of partial proofs for
independent subgoals.  The structure of these proof trees is a mixed
representation of derivation trees for the Calculus of Inductive
Constructions with abstract syntax trees for the tactics scripts,
allowing the navigation in a proof at various levels of details. The
proof engine allows generic environment items managed in an
object-oriented way.  This new architecture, due to C. Murthy,
supports several new facilities which make the system easier to extend
and to scale up:

\begin{itemize}
\item User-programmable tactics are allowed
\item It is possible to separately verify development modules, and to
  load their compiled images without verifying them again - a quick
  relocation process allows their fast loading
\item A generic parsing scheme allows user-definable notations, with a
  symmetric table-driven pretty-printer
\item Syntactic definitions allow convenient abbreviations
\item A limited facility of meta-variables allows the automatic
  synthesis of certain type expressions, allowing generic notations
  for e.g. equality, pairing, and existential quantification.
\end{itemize}

In the Fall of 1994, C. Paulin-Mohring replaced the structure of
inductively defined types and families by a new structure, allowing
the mutually recursive definitions. P. Manoury implemented a
translation of recursive definitions into the primitive recursive
style imposed by the internal recursion operators, in the style of the
ProPre system. C. Mu{\~n}oz implemented a decision procedure for
intuitionistic propositional logic, based on results of R. Dyckhoff.
J.C. Filli{\^a}tre implemented a decision procedure for first-order
logic without contraction, based on results of J. Ketonen and R.
Weyhrauch. Finally C. Murthy implemented a library of inversion
tactics, relieving the user from tedious definitions of ``inversion
predicates''.

\begin{flushright}
Rocquencourt, Feb. 1st 1995\\
Gérard Huet
\end{flushright}

\section*{Credits: addendum for version 6.1}
%\addcontentsline{toc}{section}{Credits: addendum for version V6.1}

The present version 6.1 of \Coq{} is based on the V5.10 architecture. It
was ported to the new language {\ocaml} by Bruno Barras. The
underlying framework has slightly changed and allows more conversions
between sorts. 

The new version provides powerful tools for easier developments. 

Cristina Cornes designed an extension of the \Coq{} syntax to allow
definition of terms using a powerful pattern-matching analysis in the
style of ML programs.

Amokrane Saïbi wrote a mechanism to simulate
inheritance between types families extending a proposal by Peter
Aczel. He also developed a mechanism to automatically compute which
arguments of a constant may be inferred by the system and consequently
do not need to be explicitly written. 

Yann Coscoy designed a command which explains a proof term using
natural language. Pierre Cr{\'e}gut built a new tactic which solves
problems in quantifier-free Presburger Arithmetic. Both
functionalities have been integrated to the \Coq{} system by Hugo
Herbelin.

Samuel Boutin designed a tactic for simplification of commutative
rings using a canonical set of rewriting rules and equality modulo
associativity and commutativity. 

Finally the organisation of the \Coq{} distribution has been supervised
by Jean-Christophe Filliâtre with the help of Judicaël Courant
and Bruno Barras.

\begin{flushright}
Lyon, Nov. 18th 1996\\
Christine Paulin
\end{flushright}

\section*{Credits: addendum for version 6.2}
%\addcontentsline{toc}{section}{Credits: addendum for version V6.2}

In version 6.2 of \Coq{}, the parsing is done using camlp4, a
preprocessor and pretty-printer for CAML designed by Daniel de
Rauglaudre at INRIA.  Daniel de Rauglaudre made the first adaptation
of \Coq{} for camlp4, this work was continued by Bruno Barras who also
changed the structure of \Coq{} abstract syntax trees and the primitives
to manipulate them. The result of
these changes is a faster parsing procedure with greatly improved
syntax-error messages. The user-interface to introduce grammar or
pretty-printing rules has also changed.

Eduardo Giménez redesigned the internal
tactic libraries, giving uniform names 
to Caml functions corresponding to \Coq{} tactic names. 

Bruno Barras wrote new more efficient reductions functions.

Hugo Herbelin introduced more uniform notations in the \Coq{}
specification language: the definitions by fixpoints and
pattern-matching have a more readable syntax.  Patrick Loiseleur
introduced user-friendly notations for arithmetic expressions.

New tactics were introduced: Eduardo Giménez improved a mechanism to
introduce macros for tactics, and designed special tactics for
(co)inductive definitions; Patrick Loiseleur designed a tactic to
simplify polynomial expressions in an arbitrary commutative ring which
generalizes the previous tactic implemented by Samuel Boutin.
Jean-Christophe Filli\^atre introduced a tactic for refining a goal,
using a proof term with holes as a proof scheme.

David Delahaye designed the \textsf{SearchIsos} tool to search an
object in the library given its type (up to isomorphism).

Henri Laulhère produced the \Coq{} distribution for the Windows environment.

Finally, Hugo Herbelin was the main coordinator of the \Coq{}
documentation with principal contributions by Bruno Barras, David Delahaye, 
Jean-Christophe Filli\^atre, Eduardo
Giménez, Hugo Herbelin and Patrick Loiseleur.

\begin{flushright}
Orsay, May 4th 1998\\
Christine Paulin
\end{flushright}

\section*{Credits: addendum for version 6.3}
The main changes in version V6.3 was the introduction of a few new tactics
and the extension of the guard condition for fixpoint definitions.


B. Barras extended the unification algorithm to complete partial terms
and solved various tricky bugs related to universes.\\
D. Delahaye developed the \texttt{AutoRewrite} tactic. He also designed the new
behavior of \texttt{Intro} and provided the tacticals \texttt{First} and
\texttt{Solve}.\\
J.-C. Filli\^atre developed the \texttt{Correctness} tactic.\\
E. Gim\'enez extended the guard condition in fixpoints.\\
H. Herbelin designed the new syntax for definitions and extended the
\texttt{Induction} tactic.\\
P. Loiseleur developed the \texttt{Quote} tactic and 
the new design of the \texttt{Auto}
tactic, he also introduced the index of
errors in the documentation.\\
C. Paulin wrote the \texttt{Focus} command and introduced 
the reduction functions in definitions, this last feature 
was proposed by J.-F. Monin from CNET Lannion. 

\begin{flushright}
Orsay, Dec. 1999\\
Christine Paulin
\end{flushright}

%\newpage

\section*{Credits: versions 7}

The version V7 is a new implementation started in September 1999 by
Jean-Christophe Filliâtre. This is a major revision with respect to
the internal architecture of the system.  The \Coq{} version 7.0 was
distributed in March 2001, version 7.1 in September 2001, version
7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in
February 2003.

Jean-Christophe Filliâtre designed the architecture of the new system, he
introduced a new representation for environments and wrote a new kernel
for type-checking terms. His approach was to use functional
data-structures in order to get more sharing, to prepare the addition
of modules and also to get closer to a certified kernel.

Hugo Herbelin introduced a new structure of terms with local
definitions. He introduced ``qualified'' names, wrote a new
pattern-matching compilation algorithm and designed a more compact
algorithm for checking the logical consistency of universes. He
contributed to the simplification of {\Coq} internal structures and the
optimisation of the system. He added basic tactics for forward
reasoning and coercions in patterns.

David Delahaye introduced a new language for tactics. General tactics
using pattern-matching on goals and context can directly be written
from the {\Coq} toplevel. He also provided primitives for the design
of user-defined tactics in \textsc{Caml}.

Micaela Mayero contributed the library on real numbers.
Olivier Desmettre extended this library with axiomatic
trigonometric functions, square, square roots, finite sums, Chasles
property and basic plane geometry.

Jean-Christophe Filliâtre and Pierre Letouzey redesigned a new
extraction procedure from \Coq{} terms to \textsc{Caml} or
\textsc{Haskell} programs. This new 
extraction procedure, unlike the one implemented in previous version
of \Coq{} is able to handle all terms in the Calculus of Inductive
Constructions, even involving universes and strong elimination. P.
Letouzey adapted user contributions to extract ML programs when it was
sensible.
Jean-Christophe Filliâtre wrote \verb=coqdoc=, a documentation
tool for {\Coq} libraries usable from version 7.2.

Bruno Barras improved the reduction algorithms efficiency and
the confidence level in the correctness of {\Coq} critical type-checking
algorithm.

Yves Bertot designed  the \texttt{SearchPattern} and
\texttt{SearchRewrite} tools and the support for the \textsc{pcoq} interface 
(\url{http://www-sop.inria.fr/lemme/pcoq/}).

Micaela Mayero and David Delahaye introduced {\tt Field}, a decision tactic for commutative fields.

Christine Paulin changed the elimination rules for empty and singleton
propositional inductive types.

Loïc Pottier developed {\tt Fourier}, a tactic solving linear inequalities on real numbers.

Pierre Crégut developed a new version based on reflexion of the {\tt Omega}
decision tactic.

Claudio Sacerdoti Coen designed an XML output for the {\Coq}
modules to be used in the Hypertextual Electronic Library of
Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}).

A library for efficient representation of finite maps using binary trees
contributed by Jean Goubault was integrated in the basic theories.

Pierre Courtieu developed a command and a tactic to reason on the
inductive structure of recursively defined functions.

Jacek Chrz\k{a}szcz designed and implemented the module system of
{\Coq} whose foundations are in Judicaël Courant's PhD thesis.

\bigskip

The development was coordinated by C. Paulin.

Many discussions within the Démons team and the LogiCal project
influenced significantly the design of {\Coq} especially with 
%J. Chrz\k{a}szcz, P. Courtieu, 
J. Courant, J. Duprat, J. Goubault, A. Miquel,
C. Marché, B. Monate and B. Werner.

Intensive users suggested improvements of the system :
Y. Bertot, L. Pottier, L. Théry, P. Zimmerman from INRIA,
C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D.
\begin{flushright}
Orsay, May. 2002\\
Hugo Herbelin \& Christine Paulin
\end{flushright}

\section*{Credits: version 8.0}

{\Coq} version 8 is a major revision of the {\Coq} proof assistant.
First, the underlying logic is slightly different. The so-called {\em
impredicativity} of the sort {\tt Set} has been dropped. The main
reason is that it is inconsistent with the principle of description
which is quite a useful principle for formalizing %classical
mathematics within classical logic. Moreover, even in an constructive
setting, the impredicativity of {\tt Set} does not add so much in
practice and is even subject of criticism from a large part of the
intuitionistic mathematician community. Nevertheless, the
impredicativity of {\tt Set} remains optional for users interested in
investigating mathematical developments which rely on it.

Secondly, the concrete syntax of terms has been completely
revised. The main motivations were

\begin{itemize}
\item a more uniform, purified style: all constructions are now lowercase, 
  with a functional programming perfume (e.g. abstraction is now
  written {\tt fun}), and more directly accessible to the novice
  (e.g. dependent product is now written {\tt forall} and allows
  omission of types). Also, parentheses and are no longer mandatory
  for function application.
\item extensibility: some standard notations (e.g. ``<'' and ``>'') were
  incompatible with the previous syntax. Now all standard arithmetic
  notations (=, +, *, /, <, <=, ... and more) are directly part of the
  syntax.
\end{itemize}

Together with the revision of the concrete syntax, a new mechanism of
{\em interpretation scopes} permits to reuse the same symbols
(typically +, -, *, /, <, <=) in various mathematical theories without
any ambiguities for {\Coq}, leading to a largely improved readability of
{\Coq} scripts. New commands to easily add new symbols are also
provided.

Coming with the new syntax of terms, a slight reform of the tactic
language and of the language of commands has been carried out. The
purpose here is a better uniformity making the tactics and commands
easier to use and to remember.

Thirdly, a restructuration and uniformisation of the standard library
of {\Coq} has been performed. There is now just one Leibniz' equality
usable for all the different kinds of {\Coq} objects. Also, the set of
real numbers now lies at the same level as the sets of natural and
integer numbers. Finally, the names of the standard properties of
numbers now follow a standard pattern and the symbolic
notations for the standard definitions as well.

The fourth point is the release of \CoqIDE{}, a new graphical
gtk2-based interface fully integrated to {\Coq}. Close in style from
the Proof General Emacs interface, it is faster and its integration
with {\Coq} makes interactive developments more friendly. All
mathematical Unicode symbols are usable within \CoqIDE{}.

Finally, the module system of {\Coq} completes the picture of {\Coq}
version 8.0. Though released with an experimental status in the previous
version 7.4, it should be considered as a salient feature of the new
version.

Besides, {\Coq} comes with its load of novelties and improvements: new
or improved tactics (including a new tactic for solving first-order
statements), new management commands, extended libraries.

\bigskip

Bruno Barras and Hugo Herbelin have been the main contributors of the 
reflexion and the implementation of the new syntax. The smart
automatic translator from old to new syntax released with {\Coq} is also
their work with contributions by Olivier Desmettre.

Hugo Herbelin is the main designer and implementor of the notion of
interpretation scopes and of the commands for easily adding new notations.

Hugo Herbelin is the main implementor of the restructuration of the
standard library.

Pierre Corbineau is the main designer and implementor of the new
tactic for solving first-order statements in presence of inductive
types. He is also the maintainer of the non-domain specific automation
tactics.

Benjamin Monate is the developer of the \CoqIDE{} graphical
interface with contributions by Jean-Christophe Filliâtre, Pierre
Letouzey, Claude Marché and Bruno Barras.

Claude Marché coordinated the edition of the Reference Manual for
 \Coq{} V8.0.

Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
extraction tool and module system of {\Coq}.

Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin ando
contributors from Sophia-Antipolis and Nijmegen participated to the
extension of the library.

Julien Narboux built a NSIS-based automatic {\Coq} installation tool for
the Windows platform.

Hugo Herbelin and Christine Paulin coordinated the development which
was under the responsability of Christine Paulin.

\begin{flushright}
Palaiseau \& Orsay, Apr. 2004\\
Hugo Herbelin \& Christine Paulin\\
(updated Apr. 2006)
\end{flushright}

\section*{Credits: version 8.1}

{\Coq} version 8.1 adds various new functionalities.

Benjamin Grégoire implemented an alternative algorithm to check the
convertibility of terms in the {\Coq} type-checker. This alternative
algorithm works by compilation to an efficient bytecode that is
interpreted in an abstract machine similar to Xavier Leroy's ZINC
machine.  Convertibility is performed by comparing the normal
forms. This alternative algorithm is specifically interesting for
proofs by reflection. More generally, it is convenient in case of
intensive computations.

Christine Paulin implemented an extension of inductive types allowing
recursively non uniform parameters. Hugo Herbelin implemented
sort-polymorphism for inductive types (now called template polymorphism).

Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary
compatible equivalence relations. He also generalized rewriting to
arbitrary transition systems.

Claudio Sacerdoti Coen added new features to the module system. 

Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new
more efficient and more general simplification algorithm on rings and
semi-rings.

Laurent Théry and Bruno Barras developed a new significantly more efficient
simplification algorithm on fields.

Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
Claudio Sacerdoti Coen added new tactic features.

Hugo Herbelin implemented matching on disjunctive patterns.

New mechanisms made easier the communication between {\Coq} and external
provers. Nicolas Ayache and Jean-Christophe Filliâtre implemented
connections with the provers {\sc cvcl}, {\sc Simplify} and {\sc
zenon}. Hugo Herbelin implemented an experimental protocol for calling
external tools from the tactic language.

Matthieu Sozeau developed \textsc{Russell}, an experimental language
to specify the behavior of programs with subtypes.

A mechanism to automatically use some specific tactic to solve
unresolved implicit has been implemented by Hugo Herbelin.

Laurent Théry's contribution on strings and Pierre Letouzey and
Jean-Christophe Filliâtre's contribution on finite maps have been
integrated to the {\Coq} standard library. Pierre Letouzey developed a
library about finite sets ``à la {\ocaml}''. With Jean-Marc
Notin, he extended the library on lists. Pierre Letouzey's
contribution on rational numbers has been integrated and extended..

Pierre Corbineau extended his tactic for solving first-order
statements. He wrote a reflection-based intuitionistic tautology
solver.

Pierre Courtieu, Julien Forest and Yves Bertot added extra support to
reason on the inductive structure of recursively defined functions.

Jean-Marc Notin significantly contributed to the general maintenance
of the system. He also took care of {\textsf{coqdoc}}.

Pierre Castéran contributed to the documentation of (co-)inductive
types and suggested improvements to the libraries.

Pierre Corbineau implemented a declarative mathematical proof
language, usable in combination with the tactic-based style of proof.

Finally, many users suggested improvements of the system through the
Coq-Club mailing list and bug-tracker systems, especially user groups
from INRIA Rocquencourt, Radboud University, University of
Pennsylvania and Yale University.

\enlargethispage{\baselineskip}
\begin{flushright}
Palaiseau, July 2006\\
Hugo Herbelin
\end{flushright}

\section*{Credits: version 8.2}

{\Coq} version 8.2 adds new features, new libraries and 
improves on many various aspects.

Regarding the language of Coq, the main novelty is the introduction by
Matthieu Sozeau of a package of commands providing Haskell-style
type classes. Type classes, that come with a few convenient features
such as type-based resolution of implicit arguments, plays a new role
of landmark in the architecture of Coq with respect to automatization.
For instance, thanks to type classes support, Matthieu Sozeau could
implement a new resolution-based version of the tactics dedicated to
rewriting on arbitrary transitive relations.

Another major improvement of Coq 8.2 is the evolution of the
arithmetic libraries and of the tools associated to them. Benjamin
Grégoire and Laurent Théry contributed a modular library for building
arbitrarily large integers from bounded integers while Evgeny Makarov
contributed a modular library of abstract natural and integer
arithmetics together with a few convenient tactics. On his side,
Pierre Letouzey made numerous extensions to the arithmetic libraries on
$\mathbb{Z}$ and $\mathbb{Q}$, including extra support for
automatization in presence of various number-theory concepts.

Frédéric Besson contributed a reflexive tactic based on
Krivine-Stengle Positivstellensatz (the easy way) for validating
provability of systems of inequalities. The platform is flexible enough
to support the validation of any algorithm able to produce a
``certificate'' for the Positivstellensatz and this covers the case of
Fourier-Motzkin (for linear systems in $\mathbb{Q}$ and $\mathbb{R}$),
Fourier-Motzkin with cutting planes (for linear systems in
$\mathbb{Z}$) and sum-of-squares (for non-linear systems).  Evgeny
Makarov made the platform generic over arbitrary ordered rings.

Arnaud Spiwack developed a library of 31-bits machine integers and,
relying on Benjamin Grégoire and Laurent Théry's library, delivered a
library of unbounded integers in base $2^{31}$. As importantly, he
developed a notion of ``retro-knowledge'' so as to safely extend the
kernel-located bytecode-based efficient evaluation algorithm of Coq
version 8.1 to use 31-bits machine arithmetics for efficiently
computing with the library of integers he developed.

Beside the libraries, various improvements contributed to provide a
more comfortable end-user language and more expressive tactic
language. Hugo Herbelin and Matthieu Sozeau improved the
pattern-matching compilation algorithm (detection of impossible
clauses in pattern-matching, automatic inference of the return
type). Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau contributed
various new convenient syntactic constructs and new tactics or tactic
features: more inference of redundant information, better unification,
better support for proof or definition by fixpoint, more expressive
rewriting tactics, better support for meta-variables, more convenient
notations, ...

Élie Soubiran improved the module system, adding new features (such as
an ``include'' command) and making it more flexible and more
general. He and Pierre Letouzey improved the support for modules in
the extraction mechanism.

Matthieu Sozeau extended the \textsc{Russell} language, ending in an
convenient way to write programs of given specifications, Pierre
Corbineau extended the Mathematical Proof Language and the
automatization tools that accompany it, Pierre Letouzey supervised and
extended various parts the standard library, Stéphane Glondu
contributed a few tactics and improvements, Jean-Marc Notin provided
help in debugging, general maintenance and {\tt coqdoc} support,
Vincent Siles contributed extensions of the {\tt Scheme} command and
of {\tt injection}.

Bruno Barras implemented the {\tt coqchk} tool: this is a stand-alone
type-checker that can be used to certify {\tt .vo} files. Especially,
as this verifier runs in a separate process, it is granted not to be
``hijacked'' by virtually malicious extensions added to {\Coq}.

Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and
Julien Forest acted as maintainers of features they implemented in
previous versions of Coq.

Julien Narboux contributed to {\CoqIDE}.
Nicolas Tabareau made the adaptation of the interface of the old
``setoid rewrite'' tactic to the new version. Lionel Mamane worked on
the interaction between Coq and its external interfaces. With Samuel
Mimram, he also helped making Coq compatible with recent software
tools.  Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to
improved the libraries of integers, rational, and real numbers. We
also thank many users and partners for suggestions and feedback, in
particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, 
the Foundations group at Radboud university in Nijmegen, reporters of bugs
and participants to the Coq-Club mailing list.

\begin{flushright}
Palaiseau, June 2008\\
Hugo Herbelin\\
\end{flushright}

\section*{Credits: version 8.3}

{\Coq} version 8.3 is before all a transition version with refinements
or extensions of the existing features and libraries and a new tactic
{\tt nsatz} based on Hilbert's Nullstellensatz for deciding systems of
equations over rings.

With respect to libraries, the main evolutions are due to Pierre
Letouzey with a rewriting of the library of finite sets {\tt FSets}
and a new round of evolutions in the modular development of arithmetic
(library {\tt Numbers}). The reason for making {\tt FSets} evolve is
that the computational and logical contents were quite intertwined in
the original implementation, leading in some cases to longer
computations than expected and this problem is solved in the new {\tt
  MSets} implementation. As for the modular arithmetic library, it was
only dealing with the basic arithmetic operators in the former version
and its current extension adds the standard theory of the division,
min and max functions, all made available for free to any
implementation of $\mathbb{N}$, $\mathbb{Z}$ or
$\mathbb{Z}/n\mathbb{Z}$. 

The main other evolutions of the library are due to Hugo Herbelin who
made a revision of the sorting library (includingh a certified
merge-sort) and to Guillaume Melquiond who slightly revised and
cleaned up the library of reals.

The module system evolved significantly. Besides the resolution of
some efficiency issues and a more flexible construction of module
types, Élie Soubiran brought a new model of name equivalence, the
$\Delta$-equivalence, which respects as much as possible the names
given by the users. He also designed with Pierre Letouzey a new
convenient operator \verb!<+! for nesting functor application, what
provides a light notation for inheriting the properties of cascading
modules.

The new tactic {\tt nsatz} is due to Loïc Pottier. It works by
computing Gr\"obner bases. Regarding the existing tactics, various
improvements have been done by Matthieu Sozeau, Hugo Herbelin and
Pierre Letouzey.

Matthieu Sozeau extended and refined the type classes and {\tt
  Program} features (the {\sc Russell} language). Pierre Letouzey
maintained and improved the extraction mechanism.  Bruno Barras and
\'Elie Soubiran maintained the Coq checker, Julien Forest maintained
the {\tt Function} mechanism for reasoning over recursively defined
functions. Matthieu Sozeau, Hugo Herbelin and Jean-Marc Notin
maintained {\tt coqdoc}. Frédéric Besson maintained the {\sc
  Micromega} plateform for deciding systems of inequalities. Pierre
Courtieu maintained the support for the Proof General Emacs
interface. Claude Marché maintained the plugin for calling external
provers ({\tt dp}). Yves Bertot made some improvements to the
libraries of lists and integers. Matthias Puech improved the search
functions. Guillaume Melquiond usefully contributed here and
there. Yann Régis-Gianas grounded the support for Unicode on a more
standard and more robust basis.

Though invisible from outside, Arnaud Spiwack improved the general
process of management of existential variables. Pierre Letouzey and
Stéphane Glondu improved the compilation scheme of the Coq archive.
Vincent Gross provided support to {\CoqIDE}. Jean-Marc Notin provided
support for benchmarking and archiving.

Many users helped by reporting problems, providing patches, suggesting
improvements or making useful comments, either on the bug tracker or
on the Coq-club mailing list. This includes but not exhaustively
Cédric Auger, Arthur Charguéraud, François Garillot, Georges Gonthier,
Robin Green, Stéphane Lescuyer, Eelis van der Weegen,~...

Though not directly related to the implementation, special thanks are
going to Yves Bertot, Pierre Castéran, Adam Chlipala, and Benjamin
Pierce for the excellent teaching materials they provided.

\begin{flushright}
Paris, April 2010\\
Hugo Herbelin\\
\end{flushright}

\section*{Credits: version 8.4}

{\Coq} version 8.4 contains the result of three long-term projects: a
new modular library of arithmetic by Pierre Letouzey, a new proof
engine by Arnaud Spiwack and a new communication protocol for {\CoqIDE}
by Vincent Gross.

The new modular library of arithmetic extends, generalizes and
unifies the existing libraries on Peano arithmetic (types {\tt nat},
{\tt N} and {\tt BigN}), positive arithmetic (type {\tt positive}),
integer arithmetic ({\tt Z} and {\tt BigZ}) and machine word
arithmetic (type {\tt Int31}). It provides with unified notations
(e.g. systematic use of {\tt add} and {\tt mul} for denoting the
addition and multiplication operators), systematic and generic
development of operators and properties of these operators for all the
types mentioned above, including gcd, pcm, power, square root, base 2
logarithm, division, modulo, bitwise operations, logical shifts,
comparisons, iterators, ...

The most visible feature of the new proof engine is the support for
structured scripts (bullets and proof brackets) but, even if yet not
user-available, the new engine also provides the basis for refining
existential variables using tactics, for applying tactics to several
goals simultaneously, for reordering goals, all features which are
planned for the next release. The new proof engine forced to
reimplement {\tt info} and {\tt Show Script} differently, what was
done by Pierre Letouzey.

Before version 8.4, {\CoqIDE} was linked to {\Coq} with the graphical
interface living in a separate thread. From version 8.4, {\CoqIDE} is a
separate process communicating with {\Coq} through a textual
channel. This allows for a more robust interfacing, the ability to
interrupt {\Coq} without interrupting the interface, and the ability to
manage several sessions in parallel. Relying on the infrastructure
work made by Vincent Gross, Pierre Letouzey, Pierre Boutillier and
Pierre-Marie P\'edrot contributed many various refinements of {\CoqIDE}.

{\Coq} 8.4 also comes with a bunch of many various smaller-scale changes
and improvements regarding the different components of the system.

The underlying logic has been extended with $\eta$-conversion thanks
to Hugo Herbelin, St\'ephane Glondu and Benjamin Gr\'egoire. The
addition of $\eta$-conversion is justified by the confidence that the
formulation of the Calculus of Inductive Constructions based on typed
equality (such as the one considered in Lee and Werner to build a
set-theoretic model of CIC~\cite{LeeWerner11}) is applicable to the
concrete implementation of {\Coq}.

The underlying logic benefited also from a refinement of the guard
condition for fixpoints by Pierre Boutillier, the point being that it
is safe to propagate the information about structurally smaller
arguments through $\beta$-redexes that are blocked by the
``match'' construction (blocked commutative cuts).

Relying on the added permissiveness of the guard condition, Hugo
Herbelin could extend the pattern-matching compilation algorithm
so that matching over a sequence of terms involving
dependencies of a term or of the indices of the type of a term in the
type of other terms is systematically supported.

Regarding the high-level specification language, Pierre Boutillier
introduced the ability to give implicit arguments to anonymous
functions, Hugo Herbelin introduced the ability to define notations
with several binders (e.g. \verb=exists x y z, P=), Matthieu Sozeau
made the type classes inference mechanism more robust and predictable,
Enrico Tassi introduced a command {\tt Arguments} that generalizes
{\tt Implicit Arguments} and {\tt Arguments Scope} for assigning
various properties to arguments of constants. Various improvements in
the type inference algorithm were provided by Matthieu Sozeau and Hugo
Herbelin with contributions from Enrico Tassi.

Regarding tactics, Hugo Herbelin introduced support for referring to
expressions occurring in the goal by pattern in tactics such as {\tt
  set} or {\tt destruct}. Hugo Herbelin also relied on ideas from
Chung-Kil Hur's {\tt Heq} plugin to introduce automatic computation of
occurrences to generalize when using {\tt destruct} and {\tt
  induction} on types with indices.  St\'ephane Glondu introduced new
tactics {\tt constr\_eq}, {\tt is\_evar} and {\tt has\_evar} to be
used when writing complex tactics.  Enrico Tassi added support to
fine-tuning the behavior of {\tt simpl}. Enrico Tassi added the
ability to specify over which variables of a section a lemma has
to be exactly generalized.  Pierre Letouzey added a tactic {\tt
  timeout} and the interruptibility of {\tt vm\_compute}.  Bug fixes
and miscellaneous improvements of the tactic language came from Hugo
Herbelin, Pierre Letouzey and Matthieu Sozeau.

Regarding decision tactics, Lo\"ic Pottier maintained {\tt Nsatz},
moving in particular to a type-class based reification of goals while
Fr\'ed\'eric Besson maintained {\tt Micromega}, adding in particular
support for division.

Regarding vernacular commands, St\'ephane Glondu provided new commands
to analyze the structure of type universes.

Regarding libraries, a new library about lists of a given length
(called vectors) has been provided by Pierre Boutillier. A new
instance of finite sets based on Red-Black trees and provided by
Andrew Appel has been adapted for the standard library by Pierre
Letouzey. In the library of real analysis, Yves Bertot changed the
definition of $\pi$ and provided a proof of the long-standing fact yet
remaining unproved in this library, namely that $sin \frac{\pi}{2} =
1$.

Pierre Corbineau maintained the Mathematical Proof Language (C-zar).

Bruno Barras and Benjamin Gr\'egoire maintained the call-by-value
reduction machines.

The extraction mechanism benefited from several improvements provided by
Pierre Letouzey.

Pierre Letouzey maintained the module system, with contributions from
\'Elie Soubiran.

Julien Forest maintained the {\tt Function} command.

Matthieu Sozeau maintained the setoid rewriting mechanism.

{\Coq} related tools have been upgraded too. In particular, {\tt
  coq\_makefile} has been largely revised by Pierre Boutillier. Also,
patches from Adam Chlipala for {\tt coqdoc} have been integrated by
Pierre Boutillier.

Bruno Barras and Pierre Letouzey maintained the {\tt coqchk} checker.

Pierre Courtieu and Arnaud Spiwack contributed new features for using
{\Coq} through Proof General.

The {\tt Dp} plugin has been removed. Use the plugin provided with
{\tt Why 3} instead (\url{http://why3.lri.fr}).

Under the hood, the {\Coq} architecture benefited from improvements in
terms of efficiency and robustness, especially regarding universes
management and existential variables management, thanks to Pierre
Letouzey and Yann R\'egis-Gianas with contributions from St\'ephane
Glondu and Matthias Puech. The build system is maintained by Pierre
Letouzey with contributions from St\'ephane Glondu and Pierre
Boutillier.

A new backtracking mechanism simplifying the task of external
interfaces has been designed by Pierre Letouzey.

The general maintenance was done by Pierre Letouzey, Hugo Herbelin,
Pierre Boutillier, Matthieu Sozeau and St\'ephane Glondu with also
specific contributions from Guillaume Melquiond, Julien Narboux and
Pierre-Marie Pédrot.

Packaging tools were provided by Pierre Letouzey (Windows), Pierre
Boutillier (MacOS), St\'ephane Glondu (Debian). Releasing, testing and
benchmarking support was provided by Jean-Marc Notin.

Many suggestions for improvements were motivated by feedback from
users, on either the bug tracker or the coq-club mailing list. Special
thanks are going to the users who contributed patches, starting with
Tom Prince. Other patch contributors include C\'edric Auger, David
Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson,
Hendrik Tews and Eelis van der Weegen.

\begin{flushright}
Paris, December 2011\\
Hugo Herbelin\\
\end{flushright}


\section*{Credits: version 8.5}

{\Coq} version 8.5 contains the result of five specific long-term
projects:
\begin{itemize}
\item A new asynchronous evaluation and compilation mode by Enrico
  Tassi with help from Bruno Barras and Carst Tankink.
\item Full integration of the new proof engine by Arnaud Spiwack
  helped by Pierre-Marie Pédrot,
\item Addition of conversion and reduction based on native compilation
  by Maxime Dénès and Benjamin Grégoire.
\item Full universe polymorphism for definitions and inductive types by
  Matthieu Sozeau.
\item An implementation of primitive projections with $\eta$-conversion
  bringing significant performance improvements when using records by
  Matthieu Sozeau.
\end{itemize}

The full integration of the proof engine, by Arnaud Spiwack and
Pierre-Marie Pédrot, brings to primitive tactics and the user level
Ltac language dependent subgoals, deep backtracking and multiple goal
handling, along with miscellaneous features and an improved potential
for future modifications. Dependent subgoals allow statements in a
goal to mention the proof of another. Proofs of unsolved subgoals
appear as existential variables. Primitive backtracking makes it
possible to write a tactic with several possible outcomes which are
tried successively when subsequent tactics fail. Primitives are also
available to control the backtracking behavior of tactics. Multiple
goal handling paves the way for smarter automation tactics. It is
currently used for simple goal manipulation such as goal reordering.

The way {\Coq} processes a document in batch and interactive mode has
been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
proofs, the text between Proof and Qed, can be processed
asynchronously, decoupling the checking of definitions and statements
from the checking of proofs.  It improves the responsiveness of
interactive development, since proofs can be processed in the
background.  Similarly, compilation of a file can be split into two
phases: the first one checking only definitions and statements and the
second one checking proofs.  A file resulting from the first
phase~--~with the .vio extension~--~can be already Required.  All .vio
files can be turned into complete .vo files in parallel.  The same
infrastructure also allows terminating tactics to be run in parallel
on a set of goals via the \verb=par:= goal selector.

{\CoqIDE} was modified to cope with asynchronous checking of the
document.  Its source code was also made separate from that of {\Coq}, so
that {\CoqIDE} no longer has a special status among user interfaces,
paving the way for decoupling its release cycle from that of {\Coq} in
the future.

Carst Tankink developed a {\Coq} back-end for user interfaces built on
Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander
Faithfull and Jesper Bengtson).  The development of such features was
funded by the Paral-ITP French ANR project.

The full universe polymorphism extension was designed by Matthieu
Sozeau. It conservatively extends the universes system and core calculus
with definitions and inductive declarations parameterized by universes
and constraints. It is based on a modification of the kernel architecture to
handle constraint checking only, leaving the generation of constraints
to the refinement/type inference engine. Accordingly, tactics are now
fully universe aware, resulting in more localized error messages in case
of inconsistencies and allowing higher-level algorithms like unification
to be entirely type safe. The internal representation of universes has
been modified but this is invisible to the user. 

The underlying logic has been extended with $\eta$-conversion for
records defined with primitive projections by Matthieu Sozeau. This
additional form of $\eta$-conversion is justified using the same
principle than the previously added $\eta$-conversion for function
types, based on formulations of the Calculus of Inductive Constructions
with typed equality. Primitive projections, which do not carry the
parameters of the record and are rigid names (not defined as a
pattern-matching construct), make working with nested records more
manageable in terms of time and space consumption. This extension and
universe polymorphism were carried out partly while Matthieu Sozeau was working
at the IAS in Princeton.

The guard condition has been made compliant with extensional equality
principles such as propositional extensionality and univalence, thanks to
Maxime Dénès and Bruno Barras. To ensure compatibility with the
univalence axiom, a new flag ``-indices-matter'' has been implemented, 
taking into account the universe levels of indices when computing the
levels of inductive types. This supports using {\Coq} as a tool to explore
the relations between homotopy theory and type theory.

Maxime Dénès and Benjamin Grégoire developed an implementation of
conversion test and normal form computation using the OCaml native
compiler. It complements the virtual machine conversion offering much
faster computation for expensive functions.

{\Coq} 8.5 also comes with a bunch of many various smaller-scale
changes and improvements regarding the different components of the
system. We shall only list a few of them.

Pierre Boutillier developed an improved tactic for simplification of
expressions called {\tt cbn}.

Maxime Dénès maintained the bytecode-based reduction machine. Pierre
Letouzey maintained the extraction mechanism.

Pierre-Marie Pédrot has extended the syntax of terms to,
experimentally, allow holes in terms to be solved by a locally
specified tactic.

Existential variables are referred to by identifiers rather than mere
numbers, thanks to Hugo Herbelin who also improved the tactic language
here and there.

Error messages for universe inconsistencies have been improved by
Matthieu Sozeau. Error messages for unification and type inference
failures have been improved by Hugo Herbelin, Pierre-Marie Pédrot and
Arnaud Spiwack.

Pierre Courtieu contributed new features for using {\Coq} through Proof
General and for better interactive experience (bullets, Search, etc).

The efficiency of the whole system has been significantly improved
thanks to contributions from Pierre-Marie Pédrot.

A distribution channel for {\Coq} packages using the OPAM tool has
been initiated by Thomas Braibant and developed by Guillaume Claret,
with contributions by Enrico Tassi and feedback from Hugo Herbelin.

Packaging tools were provided by Pierre Letouzey and Enrico Tassi
(Windows), Pierre Boutillier, Matthieu Sozeau and Maxime Dénès (MacOS
X). Maxime Dénès improved significantly the testing and benchmarking
support.

Many power users helped to improve the design of the new features via
the bug tracker, the coq development mailing list or the coq-club
mailing list. Special thanks are going to the users who contributed
patches and intensive brain-storming, starting with Jason Gross,
Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson,
Lionel Rieg. It would however be impossible to mention with precision
all names of people who to some extent influenced the development.

Version 8.5 is one of the most important release of {\Coq}. Its
development spanned over about 3 years and a half with about one year
of beta-testing. General maintenance during part or whole of this
period has been done by Pierre Boutillier, Pierre Courtieu, Maxime
Dénès, Hugo Herbelin, Pierre Letouzey, Guillaume Melquiond,
Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi as
well as Bruno Barras, Yves Bertot, Frédéric Besson, Xavier Clerc,
Pierre Corbineau, Jean-Christophe Filliâtre, Julien Forest, Sébastien
Hinderer, Assia Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François
Ripault, Carst Tankink. Maxime Dénès coordinated the release process.

\begin{flushright}
Paris, January 2015, revised December 2015,\\
Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
\end{flushright}

\section*{Credits: version 8.6}

{\Coq} version 8.6 contains the result of refinements, stabilization of
8.5's features and cleanups of the internals of the system. Over the
year of (now time-based) development, about 450 bugs were resolved and
over 100 contributions integrated. The main user visible changes are:
\begin{itemize}
\item A new, faster state-of-the-art universe constraint checker, by
  Jacques-Henri Jourdan.
\item In CoqIDE and other asynchronous interfaces, more fine-grained
  asynchronous processing and error reporting by Enrico Tassi, making {\Coq}
  capable of recovering from errors and continue processing the document.
\item More access to the proof engine features from Ltac: goal
  management primitives, range selectors and a {\tt typeclasses
    eauto} engine handling multiple goals and multiple successes, by
  Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.
\item Tactic behavior uniformization and specification, generalization
  of intro-patterns by Hugo Herbelin and others.
\item A brand new warning system allowing to control warnings, turn them
  into errors or ignore them selectively by Maxime Dénès, Guillaume
  Melquiond, Pierre-Marie Pédrot and others.
\item Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
\item The {\tt ssreflect} subterm selection algorithm by Georges Gonthier and
  Enrico Tassi is now accessible to tactic writers through the {\tt ssrmatching}
  plugin.
\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Jason
  Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.
\end{itemize}

{\Coq} 8.6 also comes with a bunch of smaller-scale changes and
improvements regarding the different components of the system. We shall
only list a few of them.

The {\tt iota} reduction flag is now a shorthand for {\tt match}, {\tt
  fix} and {\tt cofix} flags controlling the corresponding reduction
rules (by Hugo Herbelin and Maxime Dénès).

Maxime Dénès maintained the native compilation machinery.

Pierre-Marie Pédrot separated the Ltac code from general purpose
tactics, and generalized and rationalized the handling of generic
arguments, allowing to create new versions of Ltac more easily in the
future.

In patterns and terms, {\tt @}, abbreviations and notations are now
interpreted the same way, by Hugo Herbelin.

Name handling for universes has been improved by Pierre-Marie Pédrot and
Matthieu Sozeau. The minimization algorithm has been improved by
Matthieu Sozeau.

The unifier has been improved by Hugo Herbelin and Matthieu Sozeau,
fixing some incompatibilities introduced in Coq 8.5. Unification
constraints can now be left floating around and be seen by the user
thanks to a new option. The {\tt Keyed Unification} mode has been
improved by Matthieu Sozeau. 

The typeclass resolution engine and associated proof-search tactic have
been reimplemented on top of the proof-engine monad, providing better
integration in tactics, and new options have been introduced to control
it, by Matthieu Sozeau with help from Théo Zimmermann.

The efficiency of the whole system has been significantly improved
thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and
Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
Steckler.

Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre
Letouzey and others.

Emilio Jesús Gallego Arias contributed many cleanups and refactorings of
the pretty-printing and user interface communication components.

Frédéric Besson maintained the micromega tactic.

The OPAM repository for {\Coq} packages has been maintained by Guillaume
Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A
list of packages is now available at \url{https://coq.inria.fr/opam/www/}.

Packaging tools and software development kits were prepared by Michael
Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and
Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly
built on the continuous integration server. {\Coq} now comes with a {\tt
  META} file usable with {\tt ocamlfind}, contributed by Emilio Jesús
Gallego Arias, Gregory Malecha, and Matthieu Sozeau.

Matej Košík maintained and greatly improved the continuous integration
setup and the testing of {\Coq} contributions. He also contributed many
API improvement and code cleanups throughout the system.

The contributors for this version are Bruno Barras, C.J. Bell, Yves
Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume
Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès,
Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin,
Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy,
Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel,
Guillaume Melquiond, Clément Pit--Claudel, Pierre-Marie Pédrot, Daniel
de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote,
Matthieu Sozeau, Arnaud Spiwack, Paul Steckler, Enrico Tassi, Laurent
Théry, Nickolai Zeldovich and Théo Zimmermann. The development process
was coordinated by Hugo Herbelin and Matthieu Sozeau with the help of
Maxime Dénès, who was also in charge of the release process.

Many power users helped to improve the design of the new features via
the bug tracker, the pull request system, the {\Coq} development mailing
list or the coq-club mailing list. Special thanks to the users who
contributed patches and intensive brain-storming and code reviews,
starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan
Leivent, Xavier Leroy, Gregory Malecha, Clément Pit--Claudel, Gabriel
Scherer and Beta Ziliani. It would however be impossible to mention
exhaustively the names of everybody who to some extent influenced the
development.

Version 8.6 is the first release of {\Coq} developed on a time-based
development cycle. Its development spanned 10 months from the release of
{\Coq} 8.5 and was based on a public roadmap. To date, it contains more
external contributions than any previous {\Coq} system. Code reviews
were systematically done before integration of new features, with an
important focus given to compatibility and performance issues, resulting
in a hopefully more robust release than {\Coq} 8.5.

Coq Enhancement Proposals (CEPs for short) were introduced by Enrico
Tassi to provide more visibility and a discussion period on new
features, they are publicly available \url{https://github.com/coq/ceps}.

Started during this period, an effort is led by Yves Bertot and Maxime
Dénès to put together a {\Coq} consortium.

\begin{flushright}
Paris, November 2016,\\
Matthieu Sozeau and the {\Coq} development team\\
\end{flushright}


%new Makefile

%\newpage

% Integration of ZArith lemmas from Sophia and Nijmegen.


% $Id$ 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: