From 8f4d4c66134804bbf2d2fe65c893b68387272d31 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 10 Jul 2010 15:57:24 +0100
Subject: Remove non-DFSG contents

---
 doc/refman/RefMan-pre.tex | 783 ----------------------------------------------
 1 file changed, 783 deletions(-)
 delete mode 100644 doc/refman/RefMan-pre.tex

(limited to 'doc/refman/RefMan-pre.tex')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
deleted file mode 100644
index a2cdb5ec..00000000
--- a/doc/refman/RefMan-pre.tex
+++ /dev/null
@@ -1,783 +0,0 @@
-%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 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{\'e}gut built a new tactic which solves
-problems in quantifier-free Presburger Arithmetic. Both
-functionalities have been integrated to the \Coq{} system by Hugo
-Herbelin.
-
-Samuel Boutin designed a tactic for simplification of commutative
-rings using a canonical set of rewriting rules and equality modulo
-associativity and commutativity. 
-
-Finally the organisation of the \Coq{} distribution has been supervised
-by Jean-Christophe Filli�tre with the help of Judica�l Courant
-and Bruno Barras.
-
-\begin{flushright}
-Lyon, Nov. 18th 1996\\
-Christine Paulin
-\end{flushright}
-
-\section*{Credits: addendum for version 6.2}
-%\addcontentsline{toc}{section}{Credits: addendum for version V6.2}
-
-In version 6.2 of \Coq{}, the parsing is done using camlp4, a
-preprocessor and pretty-printer for CAML designed by Daniel de
-Rauglaudre at INRIA.  Daniel de Rauglaudre made the first adaptation
-of \Coq{} for camlp4, this work was continued by Bruno Barras who also
-changed the structure of \Coq{} abstract syntax trees and the primitives
-to manipulate them. The result of
-these changes is a faster parsing procedure with greatly improved
-syntax-error messages. The user-interface to introduce grammar or
-pretty-printing rules has also changed.
-
-Eduardo Gim�nez redesigned the internal 
-tactic libraries, giving uniform names 
-to Caml functions corresponding to \Coq{} tactic names. 
-
-Bruno Barras wrote new more efficient reductions functions.
-
-Hugo Herbelin introduced more uniform notations in the \Coq{}
-specification language: the definitions by fixpoints and
-pattern-matching have a more readable syntax.  Patrick Loiseleur
-introduced user-friendly notations for arithmetic expressions.
-
-New tactics were introduced: Eduardo Gim�nez improved a mechanism to
-introduce macros for tactics, and designed special tactics for
-(co)inductive definitions; Patrick Loiseleur designed a tactic to
-simplify polynomial expressions in an arbitrary commutative ring which
-generalizes the previous tactic implemented by Samuel Boutin.
-Jean-Christophe Filli\^atre introduced a tactic for refining a goal,
-using a proof term with holes as a proof scheme.
-
-David Delahaye designed the \textsf{SearchIsos} tool to search an
-object in the library given its type (up to isomorphism).
-
-Henri Laulh�re produced the \Coq{} distribution for the Windows environment. 
-
-Finally, Hugo Herbelin was the main coordinator of the \Coq{}
-documentation with principal contributions by Bruno Barras, David Delahaye, 
-Jean-Christophe Filli\^atre, Eduardo
-Gim�nez, Hugo Herbelin and Patrick Loiseleur. 
-
-\begin{flushright}
-Orsay, May 4th 1998\\
-Christine Paulin
-\end{flushright}
-
-\section*{Credits: addendum for version 6.3}
-The main changes in version V6.3 was the introduction of a few new tactics
-and the extension of the guard condition for fixpoint definitions.
-
-
-B. Barras extended the unification algorithm to complete partial terms
-and solved various tricky bugs related to universes.\\
-D. Delahaye developed the \texttt{AutoRewrite} tactic. He also designed the new
-behavior of \texttt{Intro} and provided the tacticals \texttt{First} and
-\texttt{Solve}.\\
-J.-C. Filli\^atre developed the \texttt{Correctness} tactic.\\
-E. Gim\'enez extended the guard condition in fixpoints.\\
-H. Herbelin designed the new syntax for definitions and extended the
-\texttt{Induction} tactic.\\
-P. Loiseleur developed the \texttt{Quote} tactic and 
-the new design of the \texttt{Auto}
-tactic, he also introduced the index of
-errors in the documentation.\\
-C. Paulin wrote the \texttt{Focus} command and introduced 
-the reduction functions in definitions, this last feature 
-was proposed by J.-F. Monin from CNET Lannion. 
-
-\begin{flushright}
-Orsay, Dec. 1999\\
-Christine Paulin
-\end{flushright}
-
-%\newpage
-
-\section*{Credits: versions 7}
-
-The version V7 is a new implementation started in September 1999 by
-Jean-Christophe Filli�tre. This is a major revision with respect to
-the internal architecture of the system.  The \Coq{} version 7.0 was
-distributed in March 2001, version 7.1 in September 2001, version
-7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in
-February 2003.
-
-Jean-Christophe Filli�tre designed the architecture of the new system, he
-introduced a new representation for environments and wrote a new kernel
-for type-checking terms. His approach was to use functional
-data-structures in order to get more sharing, to prepare the addition
-of modules and also to get closer to a certified kernel.
-
-Hugo Herbelin introduced a new structure of terms with local
-definitions. He introduced ``qualified'' names, wrote a new
-pattern-matching compilation algorithm and designed a more compact
-algorithm for checking the logical consistency of universes. He
-contributed to the simplification of {\Coq} internal structures and the
-optimisation of the system. He added basic tactics for forward
-reasoning and coercions in patterns.
-
-David Delahaye introduced a new language for tactics. General tactics
-using pattern-matching on goals and context can directly be written
-from the {\Coq} toplevel. He also provided primitives for the design
-of user-defined tactics in \textsc{Caml}.
-
-Micaela Mayero contributed the library on real numbers.
-Olivier Desmettre extended this library with axiomatic
-trigonometric functions, square, square roots, finite sums, Chasles
-property and basic plane geometry.
-
-Jean-Christophe Filli�tre and Pierre Letouzey redesigned a new
-extraction procedure from \Coq{} terms to \textsc{Caml} or
-\textsc{Haskell} programs. This new 
-extraction procedure, unlike the one implemented in previous version
-of \Coq{} is able to handle all terms in the Calculus of Inductive
-Constructions, even involving universes and strong elimination. P.
-Letouzey adapted user contributions to extract ML programs when it was
-sensible.
-Jean-Christophe Filli�tre wrote \verb=coqdoc=, a documentation
-tool for {\Coq} libraries usable from version 7.2.
-
-Bruno Barras improved the reduction algorithms efficiency and
-the confidence level in the correctness of {\Coq} critical type-checking
-algorithm.
-
-Yves Bertot designed  the \texttt{SearchPattern} and
-\texttt{SearchRewrite} tools and the support for the \textsc{pcoq} interface 
-(\url{http://www-sop.inria.fr/lemme/pcoq/}).
-
-Micaela Mayero and David Delahaye introduced {\tt Field}, a decision tactic for commutative fields.
-
-Christine Paulin changed the elimination rules for empty and singleton
-propositional inductive types.
-
-Lo�c Pottier developed {\tt Fourier}, a tactic solving linear inequalities on real numbers.
-
-Pierre Cr�gut developed a new version based on reflexion of the {\tt Omega}
-decision tactic.
-
-Claudio Sacerdoti Coen designed an XML output for the {\Coq}
-modules to be used in the Hypertextual Electronic Library of
-Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}).
-
-A library for efficient representation of finite maps using binary trees
-contributed by Jean Goubault was integrated in the basic theories.
-
-Pierre Courtieu developed a command and a tactic to reason on the
-inductive structure of recursively defined functions.
-
-Jacek Chrz\k{a}szcz designed and implemented the module system of
-{\Coq} whose foundations are in Judica�l Courant's PhD thesis.
-
-\bigskip
-
-The development was coordinated by C. Paulin.
-
-Many discussions within the D�mons team and the LogiCal project
-influenced significantly the design of {\Coq} especially with 
-%J. Chrz\k{a}szcz, P. Courtieu, 
-J. Courant, J. Duprat, J. Goubault, A. Miquel,
-C. March�, B. Monate and B. Werner.
-
-Intensive users suggested improvements of the system : 
-Y. Bertot, L. Pottier, L. Th�ry, P. Zimmerman from INRIA, 
-C. Alvarado, P. Cr�gut, J.-F. Monin from France Telecom R \& D.
-\begin{flushright}
-Orsay, May. 2002\\
-Hugo Herbelin \& Christine Paulin
-\end{flushright}
-
-\section*{Credits: version 8.0}
-
-{\Coq} version 8 is a major revision of the {\Coq} proof assistant.
-First, the underlying logic is slightly different. The so-called {\em
-impredicativity} of the sort {\tt Set} has been dropped. The main
-reason is that it is inconsistent with the principle of description
-which is quite a useful principle for formalizing %classical
-mathematics within classical logic. Moreover, even in an constructive
-setting, the impredicativity of {\tt Set} does not add so much in
-practice and is even subject of criticism from a large part of the
-intuitionistic mathematician community. Nevertheless, the
-impredicativity of {\tt Set} remains optional for users interested in
-investigating mathematical developments which rely on it.
-
-Secondly, the concrete syntax of terms has been completely
-revised. The main motivations were
-
-\begin{itemize}
-\item a more uniform, purified style: all constructions are now lowercase, 
-  with a functional programming perfume (e.g. abstraction is now
-  written {\tt fun}), and more directly accessible to the novice
-  (e.g. dependent product is now written {\tt forall} and allows
-  omission of types). Also, parentheses and are no longer mandatory
-  for function application.
-\item extensibility: some standard notations (e.g. ``<'' and ``>'') were
-  incompatible with the previous syntax. Now all standard arithmetic
-  notations (=, +, *, /, <, <=, ... and more) are directly part of the
-  syntax.
-\end{itemize}
-
-Together with the revision of the concrete syntax, a new mechanism of
-{\em interpretation scopes} permits to reuse the same symbols
-(typically +, -, *, /, <, <=) in various mathematical theories without
-any ambiguities for {\Coq}, leading to a largely improved readability of
-{\Coq} scripts. New commands to easily add new symbols are also
-provided.
-
-Coming with the new syntax of terms, a slight reform of the tactic
-language and of the language of commands has been carried out. The
-purpose here is a better uniformity making the tactics and commands
-easier to use and to remember.
-
-Thirdly, a restructuration and uniformisation of the standard library
-of {\Coq} has been performed. There is now just one Leibniz' equality
-usable for all the different kinds of {\Coq} objects. Also, the set of
-real numbers now lies at the same level as the sets of natural and
-integer numbers. Finally, the names of the standard properties of
-numbers now follow a standard pattern and the symbolic
-notations for the standard definitions as well.
-
-The fourth point is the release of \CoqIDE{}, a new graphical
-gtk2-based interface fully integrated to {\Coq}. Close in style from
-the Proof General Emacs interface, it is faster and its integration
-with {\Coq} makes interactive developments more friendly. All
-mathematical Unicode symbols are usable within \CoqIDE{}.
-
-Finally, the module system of {\Coq} completes the picture of {\Coq}
-version 8.0. Though released with an experimental status in the previous
-version 7.4, it should be considered as a salient feature of the new
-version.
-
-Besides, {\Coq} comes with its load of novelties and improvements: new
-or improved tactics (including a new tactic for solving first-order
-statements), new management commands, extended libraries.
-
-\bigskip
-
-Bruno Barras and Hugo Herbelin have been the main contributors of the 
-reflexion and the implementation of the new syntax. The smart
-automatic translator from old to new syntax released with {\Coq} is also
-their work with contributions by Olivier Desmettre.
-
-Hugo Herbelin is the main designer and implementor of the notion of
-interpretation scopes and of the commands for easily adding new notations.
-
-Hugo Herbelin is the main implementor of the restructuration of the
-standard library.
-
-Pierre Corbineau is the main designer and implementor of the new
-tactic for solving first-order statements in presence of inductive
-types. He is also the maintainer of the non-domain specific automation
-tactics.
-
-Benjamin Monate is the developer of the \CoqIDE{} graphical
-interface with contributions by Jean-Christophe Filli�tre, Pierre
-Letouzey, Claude March� and Bruno Barras.
-
-Claude March� coordinated the edition of the Reference Manual for
- \Coq{} V8.0.
-
-Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
-extraction tool and module system of {\Coq}.
-
-Jean-Christophe Filli�tre, Pierre Letouzey, Hugo Herbelin and 
-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.
-
-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 Objective Caml''. With Jean-Marc
-Notin, he extended the library on lists. Pierre Letouzey's
-contribution on rational numbers has been integrated and extended..
-
-Pierre Corbineau extended his tactic for solving first-order
-statements. He wrote a reflection-based intuitionistic tautology
-solver.
-
-Pierre Courtieu, Julien Forest and Yves Bertot added extra support to
-reason on the inductive structure of recursively defined functions.
-
-Jean-Marc Notin significantly contributed to the general maintenance
-of the system. He also took care of {\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, Radbout 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 Radbout 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}
-
-%new Makefile
-
-%\newpage
-
-% Integration of ZArith lemmas from Sophia and Nijmegen.
-
-
-% $Id: RefMan-pre.tex 13271 2010-07-08 18:10:54Z herbelin $ 
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
-- 
cgit v1.2.3

