Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into aspiwack-render-prehistory3

Pull request #120

2 files changed, 378 insertions, 296 deletions

diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5
deleted file mode 100644
index ebbc057734..0000000000
--- a/dev/doc/README-V1-V5
+++ /dev/null
@@ -1,296 +0,0 @@
-
-                 Notes on the prehistory of Coq
-
-This document is a copy within the Coq archive of a document written
-in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin
-to accompany their public release of the archive of versions 1.10 to 6.2
-of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and
-implemented in the Formel team, joint between the INRIA Rocquencourt
-laboratory and the Ecole Normale Supérieure of Paris, from 1984
-onwards.
-
-Version 1
-
-This software is a prototype type-checker for a higher-order logical formalism
-known as the Theory of Constructions, presented in his PhD thesis by
-Thierry Coquand, with influences from Girard's system F and de Bruijn's Automath.
-The metamathematical analysis of the system is the
-PhD work of Thierry Coquand. The software is mostly the work of Gérard Huet.
-Most of the mathematical examples verified with the software are due
-to Thierry Coquand.
-
-The programming language of the CONSTR software (as it was called at the time)
-is a version of ML issued from the Edinburgh LCF system and running on
-a LISP backend. The main improvements from the original LCF ML are that ML
-is compiled rather than interpreted (Gérard Huet building on the original
-translator by Lockwood Morris), and that it is enriched by recursively
-defined types (work of Guy Cousineau). This ancestor of CAML was used
-and improved by Larry Paulson for his implementation of Cambridge LCF.
-
-Software developments of this prototype occurred from late 1983 to early 1985.
-
-Version 1.10 was frozen on December 22nd 1984. It is the version used for the
-examples in Thierry Coquand's thesis, defended on January 31st 1985.
-There was a unique binding operator, used both for universal quantification
-(dependent product) at the level of types and functional abstraction (lambda)
-at the level of terms/proofs, in the manner of Automath. Substitution
-(lambda reduction) was implemented using de Bruijn's indexes.
-
-Version 1.11 was frozen on February 19th, 1985. It is the version used for the
-examples in the paper:
-Th. Coquand, G. Huet. Constructions: A Higher Order Proof System for Mechanizing
-Mathematics. Invited paper, EUROCAL85, April 1985, Linz, Austria. Springer Verlag
-LNCS 203, pp. 151-184.
-
-Christine Paulin joined the team at this point, for her DEA research internship.
-In her DEA memoir (August 1985) she presents developments for the lambo function
-computing the minimal m such that f(m) is greater than n, for f an increasing
-integer function, a challenge for constructive mathematics. She also encoded
-the majority voting algorithm of Boyer and Moore.
-
-Version 2
-
-The formal system, now renamed as the "Calculus of Constructions", was presented
-with a proof of consistency and comparisons with proof systems of Per
-Martin Löf, Girard, and the Automath family of N. de Bruijn, in the paper:
-T. Coquand and G. Huet. The Calculus of Constructions.
-Submitted on June 30th 1985, accepted on December 5th, 1985,
-Information and Computation. Preprint as Rapport de Recherche Inria n°530,
-Mai 1986. Final version in Information and Computation 76,2/3, Feb. 88.
-
-An abstraction of the software design, in the form of an abstract machine
-for proof checking, and a fuller sequence of mathematical developments was
-presented in:
-Th. Coquand, G. Huet. Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions. Invited paper, European Logic Colloquium, Orsay,
-July 1985. Preprint as Rapport de recherche INRIA n°463, Dec. 85.
-Published in Logic Colloquium 1985, North-Holland, 1987.
-
-Version 2.8 was frozen on December 16th, 1985, and served for developing
-the exemples in the above papers.
-
-This calculus was then enriched in version 2.9 with a cumulative hierarchy of
-universes. Universe levels were initially explicit natural numbers.
-Another improvement was the possibility of automatic synthesis of implicit
-type arguments, relieving the user of tedious redundant declarations.
-
-Christine Paulin wrote an article "Algorithm development in the Calculus of
-Constructions", preprint as Rapport de recherche INRIA n°497, March 86.
-Final version in Proceedings Symposium on Logic in Computer Science, Cambridge,
-MA, 1986 (IEEE Computer Society Press). Besides lambo and majority,
-she presents quicksort and a text formatting algorithm.
-
-Version 2.13 of the calculus of constructions with universes was frozen
-on June 25th, 1986.
-
-A synthetic presentation of type theory along constructive lines with ML
-algorithms was given by Gérard Huet in his May 1986 CMU course notes
-"Formal Structures for Computation and Deduction". Its chapter
-"Induction and Recursion in the Theory of Constructions" was presented
-as an invited paper at the Joint Conference on Theory and Practice of Software
-Development TAPSOFT’87 at Pise in March 1987, and published as
-"Induction Principles Formalized in the Calculus of Constructions" in
-Programming of Future Generation Computers, Ed. K. Fuchi and M. Nivat,
-North-Holland, 1988.
-
-Version 3
-
-This version saw the beginning of proof automation, with a search algorithm
-inspired from PROLOG and the applicative logic programming programs
-of the course notes "Formal structures for computation and deduction".
-The search algorithm was implemented in ML by Thierry Coquand.
-The proof system could thus be used in two modes: proof verification and
-proof synthesis, with tactics such as "AUTO".
-
-The implementation language was now called CAML, for "categorical abstract
-machine language". It used as backend the LLM3 virtual machine of Le Lisp
-by Jérôme Chailloux. The main developers of CAML were Michel Mauny,
-Ascander Suarez and Pierre Weis.
-
-V3.1 was started in the summer of 1986, V3.2 was frozen at the end of November
-1986. V3.4 was developed in the first half of 1987.
-
-Thierry Coquand held a post-doctoral position in Cambrige University in 1986-87,
-where he developed a variant implementation in SML, with which he wrote
-some developments on fixpoints in Scott's domains.
-
-Version 4
-
-This version saw the beginning of program extraction from proofs, with
-two varieties of the type Prop of propositions, indicating constructive intent.
-The proof extraction algorithms were implemented by Christine Paulin-Mohring.
-
-V4.1 was frozen on July 24th, 1987. It had a first identified library of
-mathematical developments (directory exemples), with libraries Logic
-(containing impredicative encodings of intuitionistic logic and algebraic
-primitives for booleans, natural numbers and list), Peano developing second-order
-Peano arithmetic, Arith defining addition, multiplication, euclidean division
-and factorial. Typical developments were the Knaster-Tarski theorem
-and Newman's lemma from rewriting theory.
-
-V4.2 was a joint development of a team consisting of Thierry Coquand, Gérard
-Huet and Christine Paulin-Mohring. A file V4.2.log records the log of changes.
-It was frozen on September 1987 as the last version implemented in CAML 2.3,
-and V4.3 followed on CAML 2.5, a more stable development system.
-
-V4.3 saw the first top-level of the system. Instead of evaluating explicit
-quotations, the user could develop his mathematics in a high-level language
-called the mathematical vernacular (following Automath terminology).
-The user could develop files in the vernacular notation (with .v extension)
-which were now separate from the ml sources of the implementation.
-Gilles Dowek joined the team to develop the vernacular language as his
-DEA internship research.
-
-A notion of sticky constant was introduced, in order to keep names of lemmas
-when local hypotheses of proofs were discharged. This gave a notion
-of global mathematical environment with local sections.
-
-Another significant practical change was that the system, originally developped
-on the VAX central computer of our lab, was transferred on SUN personal
-workstations, allowing a level of distributed development.
-The extraction algorithm was modified, with three annotations Pos, Null and
-Typ decorating the sorts Prop and Type.
-
-Version 4.3 was frozen at the end of November 1987, and was distributed to an
-early community of users (among those were Hugo Herbelin and Loic Colson).
-
-V4.4 saw the first version of (encoded) inductive types.
-Now natural numbers could be defined as:
-Inductive NAT : Prop = O : NAT | Succ : NAT->NAT.
-These inductive types were encoded impredicatively in the calculus,
-using a subsystem "rec" due to Christine Paulin.
-V4.4 was frozen on March 6th 1988.
-
-Version 4.5 was the first one to support inductive types and program extraction.
-Its banner was "Calcul des Constructions avec Realisations et Synthese".
-The vernacular language was enriched to accommodate extraction commands.
-
-The verification engine design was presented as:
-G. Huet. The Constructive Engine. Version 4.5. Invited Conference, 2nd European
-Symposium on Programming, Nancy, March 88.
-The final paper, describing the V4.9 implementation, appeared in:
-A perspective in Theoretical Computer Science, Commemorative Volume in memory
-of Gift Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.
-
-Version 4.5 was demonstrated in June 1988 at the YoP Institute on Logical
-Foundations of Functional Programming organized by Gérard Huet at Austin, Texas.
-
-Version 4.6 was started during summer 1988. Its main improvement was the
-complete rehaul of the proof synthesis engine by Thierry Coquand, with
-a tree structure of goals.
-
-Its source code was communicated to Randy Pollack on September 2nd 1988.
-It evolved progressively into LEGO, proof system for Luo's formalism
-of Extended Calculus of Constructions.
-
-The discharge tactic was modified by G. Huet to allow for inter-dependencies
-in discharged lemmas. Christine Paulin improved the inductive definition scheme
-in order to accommodate predicates of any arity.
-
-Version 4.7 was started on September 6th, 1988.
-
-This version starts exploiting the CAML notion of module in order to improve the
-modularity of the implementation. Now the term verifier is identified as
-a proper module Machine, which the structure of its internal data structures
-being hidden and thus accessible only through the legitimate operations.
-This machine (the constructive engine) was the trusted core of the
-implementation. The proof synthesis mechanism was a separate proof term
-generator. Once a complete proof term was synthesized with the help of tactics,
-it was entirely re-checked by the engine. Thus there was no need to certify
-the tactics, and the system took advantage of this fact by having tactics ignore
-the universe levels, universe consistency check being relegated to the final
-type-checking pass. This induced a certain puzzlement of early users who saw
-their successful proof search ended with QED, followed by silence, followed by
-a failure message of universe inconsistency rejection...
-
-The set of examples comprise set theory experiments by Hugo Herbelin,
-and notably the Schroeder-Bernstein theorem.
-
-Version 4.8, started on October 8th, 1988, saw a major re-implementation of the
-abstract syntax type constr, separating variables of the formalism and
-metavariables denoting incomplete terms managed by the search mechanism.
-A notion of level (with three values TYPE, OBJECT and PROOF) is made explicit
-and a type judgement clarifies the constructions, whose implementation is now
-fully explicit. Structural equality is speeded up by using pointer equality,
-yielding spectacular improvements. Thierry Coquand adapts the proof synthesis
-to the new representation, and simplifies pattern matching to 1st order
-predicate calculus matching, with important performance gain.
-
-A new representation of the universe hierarchy is then defined by G. Huet.
-Universe levels are now implemented implicitly, through a hidden graph
-of abstract levels constrained with an order relation.
-Checking acyclicity of the graph insures well-foundedness of the ordering,
-and thus consistency. This was documented in a memo
-"Adding Type:Type to the Calculus of Constructions" which was never published.
-
-The development version is released as a stable 4.8 at the end of 1988.
-
-Version 4.9 is released on March 1st 1989, with the new "elastic"
-universe hierarchy.
-
-The spring 89 saw the first attempt at documenting the system usage,
-with a number of papers describing the formalism:
-- Metamathematical Investigations of a Calculus of Constructions, by
-Thierry Coquand (INRIA Research Report N°1088, Sept. 1989, published in
-Logic and Computer Science, ed. P.G. Odifreddi, Academic Press, 1990)
-- Inductive definitions in the Calculus of Constructions, by
-Christine Paulin-Mohring,
-- Extracting Fomega's programs from proofs in the Calculus of Constructions, by
-Christine Paulin-Mohring (published in POPL'89)
-- The Constructive Engine, by Gérard Huet
-as well as a number of user guides:
-- A short user's guide for the Constructions Version 4.10, by Gérard Huet
-- A Vernacular Syllabus, by Gilles Dowek.
-- The Tactics Theorem Prover, User's guide, Version 4.10, by Thierry Coquand.
-
-Stable V4.10, released on May 1st, 1989, was then a mature system,
-distributed with CAML V2.6.
-
-In the mean time, Thierry Coquand and Christine Paulin-Mohring
-had been investigating how to add native inductive types to the
-Calculus of Constructions, in the manner of Per Martin-Löf's Intuitionistic
-Type Theory. The impredicative encoding had already been presented in:
-F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus
-of Constructions. Preprint technical report CMU-CS-89-209, final version in
-Proceedings of Mathematical Foundations of Programming Semantics,
-volume 442, Lecture Notes in Computer Science. Springer-Verlag, 1990.
-An extension of the calculus with primitive inductive types appeared in:
-Th. Coquand and C. Paulin-Mohring. Inductively defined types.
-In P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88, volume 417,
-Lecture Notes in Computer Science. Springer-Verlag, 1990.
-
-This lead to the Calculus of Inductive Constructions, logical formalism
-implemented in Versions 5 upward of the system, and documented in:
-C. Paulin-Mohring. Inductive Definitions in the System Coq - Rules and
-Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference
-Typed Lambda Calculi and Applications, volume 664, Lecture Notes in Computer
-Science, 1993.
-
-The last version of CONSTR is Version 4.11, which was last distributed
-in Spring 1990. It was demonstrated at the first workshop of the European
-Basic Research Action Logical Frameworks In Sophia Antipolis in May 1990.
-
-At the end of 1989, Version 5.1 was started, and renamed as the system Coq
-for the Calculus of Inductive Constructions. It was then ported to the new
-stand-alone implementation of ML called Caml-light.
-
-In 1990 many changes occurred. Thierry Coquand left for Chalmers University
-in Göteborg. Christine Paulin-Mohring took a CNRS researcher position
-at the LIP laboratory of Ecole Normale Supérieure de Lyon. Project Formel
-was terminated, and gave rise to two teams: Cristal at INRIA-Roquencourt,
-that continued developments in functional programming with Caml-light then
-Ocaml, and Coq, continuing the type theory research, with a joint team
-headed by Gérard Huet at INRIA-Rocquencourt and Christine Paulin-Mohring
-at the LIP laboratory of CNRS-ENS Lyon.
-
-Chetan Murthy joined the team in 1991 and became the main software architect
-of Version 5. He completely rehauled the implementation for efficiency.
-Versions 5.6 and 5.8 were major distributed versions, with complete
-documentation and a library of users' developements. The use of the RCS
-revision control system, and systematic ChangeLog files, allow a more
-precise tracking of the software developments.
-
-Developments from Version 6 upwards are documented in the credits section of
-Coq's Reference Manual.
-
-September 2015
-Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.
diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc
new file mode 100644
index 0000000000..631fb92c97
--- /dev/null
+++ b/dev/doc/README-V1-V5.asciidoc
@@ -0,0 +1,378 @@
+Notes on the prehistory of Coq
+==============================
+:author:  Thierry Coquand, Gérard Huet & Christine Paulin-Mohring
+:revdate: September 2015
+:toc:
+:toc-placement: preamble
+:toclevels: 1
+:showtitle:
+
+
+This document is a copy within the Coq archive of a document written
+in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin
+to accompany their public release of the archive of versions 1.10 to 6.2
+of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and
+implemented in the Formel team, joint between the INRIA Rocquencourt
+laboratory and the Ecole Normale Supérieure of Paris, from 1984
+onwards.
+
+Version 1
+---------
+
+This software is a prototype type-checker for a higher-order logical
+formalism known as the Theory of Constructions, presented in his PhD
+thesis by Thierry Coquand, with influences from Girard's system F and
+de Bruijn's Automath.  The metamathematical analysis of the system is
+the PhD work of Thierry Coquand. The software is mostly the work of
+Gérard Huet.  Most of the mathematical examples verified with the
+software are due to Thierry Coquand.
+
+The programming language of the CONSTR software (as it was called at
+the time) was a version of ML adapted from the Edinburgh LCF system
+and running on a LISP backend. The main improvements from the original
+LCF ML were that ML was compiled rather than interpreted (Gérard Huet
+building on the original translator by Lockwood Morris), and that it
+was enriched by recursively defined types (work of Guy
+Cousineau). This ancestor of CAML was used and improved by Larry
+Paulson for his implementation of Cambridge LCF.
+
+Software developments of this prototype occurred from late 1983 to
+early 1985.
+
+Version 1.10 was frozen on December 22nd 1984. It is the version used
+for the examples in Thierry Coquand's thesis, defended on January 31st
+1985.  There was a unique binding operator, used both for universal
+quantification (dependent product) at the level of types and
+functional abstraction (λ) at the level of terms/proofs, in the manner
+of Automath. Substitution (λ-reduction) was implemented using de
+Bruijn's indexes.
+
+Version 1.11 was frozen on February 19th, 1985. It is the version used
+for the examples in the paper: Th. Coquand, G. Huet. __Constructions: A
+Higher Order Proof System for Mechanizing Mathematics__ <<CH85>>.
+
+Christine Paulin joined the team at this point, for her DEA research
+internship.  In her DEA memoir (August 1985) she presents developments
+for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such
+that _f(m)_ is greater than _n_, for _f_ an increasing integer
+function, a challenge for constructive mathematics. She also encoded
+the majority voting algorithm of Boyer and Moore.
+
+Version 2
+---------
+
+The formal system, now renamed as the _Calculus of Constructions_, was
+presented with a proof of consistency and comparisons with proof
+systems of Per Martin Löf, Girard, and the Automath family of N. de
+Bruijn, in the paper: T. Coquand and G. Huet. __The Calculus of
+Constructions__ <<CH88>>.
+
+An abstraction of the software design, in the form of an abstract
+machine for proof checking, and a fuller sequence of mathematical
+developments was presented in: Th. Coquand, G. Huet. __Concepts
+Mathématiques et Informatiques Formalisés dans le Calcul des
+Constructions__<<CH87>>.
+
+Version 2.8 was frozen on December 16th, 1985, and served for
+developing the exemples in the above papers.
+
+This calculus was then enriched in version 2.9 with a cumulative
+hierarchy of universes. Universe levels were initially explicit
+natural numbers.  Another improvement was the possibility of automatic
+synthesis of implicit type arguments, relieving the user of tedious
+redundant declarations.
+
+Christine Paulin wrote an article __Algorithm development in the
+Calculus of Constructions__ <<P86>>. Besides _lambo_ and _majority_,
+she presents quicksort and a text formatting algorithm.
+
+Version 2.13 of the Calculus of Constructions with universes was
+frozen on June 25th, 1986.
+
+A synthetic presentation of type theory along constructive lines with
+ML algorithms was given by Gérard Huet in his May 1986 CMU course
+notes _Formal Structures for Computation and Deduction_. Its chapter
+_Induction and Recursion in the Theory of Constructions_ was presented
+as an invited paper at the Joint Conference on Theory and Practice of
+Software Development TAPSOFT’87 at Pise in March 1987, and published
+as __Induction Principles Formalized in the Calculus of
+Constructions__ <<H88>>.
+
+Version 3
+---------
+
+This version saw the beginning of proof automation, with a search
+algorithm inspired from PROLOG and the applicative logic programming
+programs of the course notes _Formal structures for computation and
+deduction_.  The search algorithm was implemented in ML by Thierry
+Coquand.  The proof system could thus be used in two modes: proof
+verification and proof synthesis, with tactics such as `AUTO`.
+
+The implementation language was now called CAML, for Categorical
+Abstract Machine Language. It used as backend the LLM3 virtual machine
+of Le Lisp by Jérôme Chailloux. The main developers of CAML were
+Michel Mauny, Ascander Suarez and Pierre Weis.
+
+V3.1 was started in the summer of 1986, V3.2 was frozen at the end of
+November 1986. V3.4 was developed in the first half of 1987.
+
+Thierry Coquand held a post-doctoral position in Cambrige University
+in 1986-87, where he developed a variant implementation in SML, with
+which he wrote some developments on fixpoints in Scott's domains.
+
+Version 4
+---------
+
+This version saw the beginning of program extraction from proofs, with
+two varieties of the type `Prop` of propositions, indicating
+constructive intent.  The proof extraction algorithms were implemented
+by Christine Paulin-Mohring.
+
+V4.1 was frozen on July 24th, 1987. It had a first identified library
+of mathematical developments (directory exemples), with libraries
+Logic (containing impredicative encodings of intuitionistic logic and
+algebraic primitives for booleans, natural numbers and list), `Peano`
+developing second-order Peano arithmetic, `Arith` defining addition,
+multiplication, euclidean division and factorial. Typical developments
+were the Knaster-Tarski theorem and Newman's lemma from rewriting
+theory.
+
+V4.2 was a joint development of a team consisting of Thierry Coquand,
+Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the
+log of changes.  It was frozen on September 1987 as the last version
+implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable
+development system.
+
+V4.3 saw the first top-level of the system. Instead of evaluating
+explicit quotations, the user could develop his mathematics in a
+high-level language called the mathematical vernacular (following
+Automath terminology).  The user could develop files in the vernacular
+notation (with .v extension) which were now separate from the `ml`
+sources of the implementation.  Gilles Dowek joined the team to
+develop the vernacular language as his DEA internship research.
+
+A notion of sticky constant was introduced, in order to keep names of
+lemmas when local hypotheses of proofs were discharged. This gave a
+notion of global mathematical environment with local sections.
+
+Another significant practical change was that the system, originally
+developped on the VAX central computer of our lab, was transferred on
+SUN personal workstations, allowing a level of distributed
+development.  The extraction algorithm was modified, with three
+annotations `Pos`, `Null` and `Typ` decorating the sorts `Prop` and
+`Type`.
+
+Version 4.3 was frozen at the end of November 1987, and was
+distributed to an early community of users (among those were Hugo
+Herbelin and Loic Colson).
+
+V4.4 saw the first version of (encoded) inductive types.  Now natural
+numbers could be defined as:
+
+[source, coq]
+Inductive NAT : Prop = O : NAT | Succ : NAT->NAT.
+
+These inductive types were encoded impredicatively in the calculus,
+using a subsystem _rec_ due to Christine Paulin.  V4.4 was frozen on
+March 6th 1988.
+
+Version 4.5 was the first one to support inductive types and program
+extraction.  Its banner was _Calcul des Constructions avec
+Réalisations et Synthèse_.  The vernacular language was enriched to
+accommodate extraction commands.
+
+The verification engine design was presented as: G. Huet. _The
+Constructive Engine_. Version 4.5. Invited Conference, 2nd European
+Symposium on Programming, Nancy, March 88.  The final paper,
+describing the V4.9 implementation, appeared in: A perspective in
+Theoretical Computer Science, Commemorative Volume in memory of Gift
+Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.
+
+Version 4.5 was demonstrated in June 1988 at the YoP Institute on
+Logical Foundations of Functional Programming organized by Gérard Huet
+at Austin, Texas.
+
+Version 4.6 was started during the summer of 1988. Its main
+improvement was the complete rehaul of the proof synthesis engine by
+Thierry Coquand, with a tree structure of goals.
+
+Its source code was communicated to Randy Pollack on September 2nd
+1988.  It evolved progressively into LEGO, proof system for Luo's
+formalism of Extended Calculus of Constructions.
+
+The discharge tactic was modified by Gérard Huet to allow for
+inter-dependencies in discharged lemmas. Christine Paulin improved the
+inductive definition scheme in order to accommodate predicates of any
+arity.
+
+Version 4.7 was started on September 6th, 1988.
+
+This version starts exploiting the CAML notion of module in order to
+improve the modularity of the implementation. Now the term verifier is
+identified as a proper module Machine, which the structure of its
+internal data structures being hidden and thus accessible only through
+the legitimate operations.  This machine (the constructive engine) was
+the trusted core of the implementation. The proof synthesis mechanism
+was a separate proof term generator. Once a complete proof term was
+synthesized with the help of tactics, it was entirely re-checked by
+the engine. Thus there was no need to certify the tactics, and the
+system took advantage of this fact by having tactics ignore the
+universe levels, universe consistency check being relegated to the
+final type-checking pass. This induced a certain puzzlement in early
+users who saw, after a successful proof search, their `QED` followed
+by silence, followed by a failure message due to a universe
+inconsistency…
+
+The set of examples comprise set theory experiments by Hugo Herbelin,
+and notably the Schroeder-Bernstein theorem.
+
+Version 4.8, started on October 8th, 1988, saw a major
+re-implementation of the abstract syntax type `constr`, separating
+variables of the formalism and metavariables denoting incomplete terms
+managed by the search mechanism.  A notion of level (with three values
+`TYPE`, `OBJECT` and `PROOF`) is made explicit and a type judgement
+clarifies the constructions, whose implementation is now fully
+explicit. Structural equality is speeded up by using pointer equality,
+yielding spectacular improvements. Thierry Coquand adapts the proof
+synthesis to the new representation, and simplifies pattern matching
+to first-order predicate calculus matching, with important performance
+gain.
+
+A new representation of the universe hierarchy is then defined by
+Gérard Huet.  Universe levels are now implemented implicitly, through
+a hidden graph of abstract levels constrained with an order relation.
+Checking acyclicity of the graph insures well-foundedness of the
+ordering, and thus consistency. This was documented in a memo _Adding
+Type:Type to the Calculus of Constructions_ which was never published.
+
+The development version is released as a stable 4.8 at the end of
+1988.
+
+Version 4.9 is released on March 1st 1989, with the new ``elastic''
+universe hierarchy.
+
+The spring of 1989 saw the first attempt at documenting the system
+usage, with a number of papers describing the formalism:
+
+- _Metamathematical Investigations of a Calculus of Constructions_, by
+  Thierry Coquand <<C90>>,
+- _Inductive definitions in the Calculus of Constructions_, by
+   Christine Paulin-Mohrin,
+- _Extracting Fω's programs from proofs in the Calculus of
+  Constructions_, by Christine Paulin-Mohring <<P89>>,
+- _The Constructive Engine_, by Gérard Huet <<H89>>,
+
+as well as a number of user guides:
+
+- _A short user's guide for the Constructions_ Version 4.10, by Gérard Huet
+- _A Vernacular Syllabus_, by Gilles Dowek.
+- _The Tactics Theorem Prover, User's guide_, Version 4.10, by Thierry
+  Coquand.
+
+Stable V4.10, released on May 1st, 1989, was then a mature system,
+distributed with CAML V2.6.
+
+In the mean time, Thierry Coquand and Christine Paulin-Mohring had
+been investigating how to add native inductive types to the Calculus
+of Constructions, in the manner of Per Martin-Löf's Intuitionistic
+Type Theory. The impredicative encoding had already been presented in:
+F. Pfenning and C. Paulin-Mohring. __Inductively defined types in the
+Calculus of Constructions__ <<PP90>>. An extension of the calculus
+with primitive inductive types appeared in: Th. Coquand and
+C. Paulin-Mohring. __Inductively defined types__ <<CP90>>.
+
+This led to the Calculus of Inductive Constructions, logical formalism
+implemented in Versions 5 upward of the system, and documented in:
+C. Paulin-Mohring. __Inductive Definitions in the System Coq - Rules
+and Properties__ <<P93>>.
+
+The last version of CONSTR is Version 4.11, which was last distributed
+in the spring of 1990. It was demonstrated at the first workshop of
+the European Basic Research Action Logical Frameworks In Sophia
+Antipolis in May 1990.
+
+At the end of 1989, Version 5.1 was started, and renamed as the system
+Coq for the Calculus of Inductive Constructions. It was then ported to
+the new stand-alone implementation of ML called Caml-light.
+
+In 1990 many changes occurred. Thierry Coquand left for Chalmers
+University in Göteborg. Christine Paulin-Mohring took a CNRS
+researcher position at the LIP laboratory of École Normale Supérieure
+de Lyon. Project Formel was terminated, and gave rise to two teams:
+Cristal at INRIA-Roquencourt, that continued developments in
+functional programming with Caml-light then Ocaml, and Coq, continuing
+the type theory research, with a joint team headed by Gérard Huet at
+INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory
+of CNRS-ENS Lyon.
+
+Chetan Murthy joined the team in 1991 and became the main software
+architect of Version 5. He completely rehauled the implementation for
+efficiency.  Versions 5.6 and 5.8 were major distributed versions,
+with complete documentation and a library of users' developements. The
+use of the RCS revision control system, and systematic ChangeLog
+files, allow a more precise tracking of the software developments.
+
+Developments from Version 6 upwards are documented in the credits
+section of Coq's Reference Manual.
+
+====
+September 2015 +
+Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.
+====
+
+[bibliography]
+.Bibliographic references
+
+- [[[CH85]]] Th. Coquand, G. Huet. _Constructions: A Higher Order
+  Proof System for Mechanizing Mathematics_. Invited paper, EUROCAL85,
+  April 1985, Linz, Austria. Springer Verlag LNCS 203, pp. 151-184.
+
+- [[[CH88]]] T. Coquand and G. Huet. _The Calculus of Constructions_.
+  Submitted on June 30th 1985, accepted on December 5th, 1985,
+  Information and Computation. Preprint as Rapport de Recherche Inria
+  n°530, Mai 1986. Final version in Information and Computation
+  76,2/3, Feb. 88.
+
+- [[[CH87]]] Th. Coquand, G. Huet. _Concepts Mathématiques et
+  Informatiques Formalisés dans le Calcul des Constructions_. Invited
+  paper, European Logic Colloquium, Orsay, July 1985. Preprint as
+  Rapport de recherche INRIA n°463, Dec. 85.  Published in Logic
+  Colloquium 1985, North-Holland, 1987.
+
+- [[[P86]]] C. Paulin. _Algorithm development in the Calculus of
+  Constructions_, preprint as Rapport de recherche INRIA n°497,
+  March 86. Final version in Proceedings Symposium on Logic in Computer
+  Science, Cambridge, MA, 1986 (IEEE Computer Society Press).
+
+- [[[H88]]] G. Huet. _Induction Principles Formalized in the Calculus
+  of Constructions_ in Programming of Future Generation Computers,
+  Ed. K. Fuchi and M. Nivat, North-Holland, 1988.
+
+- [[[C90]]] Th. Coquand. _Metamathematical Investigations of a
+  Calculus of Constructions_, by INRIA Research Report N°1088,
+  Sept. 1989, published in Logic and Computer Science,
+  ed. P.G. Odifreddi, Academic Press, 1990.
+
+- [[[P89]]] C. Paulin. _Extracting F ω's programs from proofs in the
+  calculus of constructions_. 16th Annual ACM Symposium on Principles
+  of Programming Languages, Austin. 1989.
+
+- [[[H89]]] G. Huet. _The constructive engine_. A perspective in
+  Theoretical Computer Science. Commemorative Volume for Gift
+  Siromoney. World Scientific Publishing (1989).
+
+- [[[PP90]]] F. Pfenning and C. Paulin-Mohring. _Inductively defined
+  types in the Calculus of Constructions_. Preprint technical report
+  CMU-CS-89-209, final version in Proceedings of Mathematical
+  Foundations of Programming Semantics, volume 442, Lecture Notes in
+  Computer Science. Springer-Verlag, 1990
+
+- [[[CP90]]] Th. Coquand and C. Paulin-Mohring. _Inductively defined
+  types_.  In P. Martin-Löf and G. Mints, editors, Proceedings of
+  Colog'88, volume 417, Lecture Notes in Computer Science.
+  Springer-Verlag, 1990.
+
+- [[[P93]]] C. Paulin-Mohring. _Inductive Definitions in the System
+  Coq - Rules and Properties_. In M. Bezem and J.-F. Groote, editors,
+  Proceedings of the conference Typed Lambda Calculi and Applications,
+  volume 664, Lecture Notes in Computer Science, 1993.