Prehistory of Coq: justification of the plain text.

1 files changed, 254 insertions, 229 deletions

diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc
index a02f0831dc..4395fd0e5c 100644
--- a/dev/doc/README-V1-V5.asciidoc
+++ b/dev/doc/README-V1-V5.asciidoc
@@ -8,44 +8,47 @@ Notes on the prehistory of Coq
 :showtitle:
 
 
-This archive contains the sources of the CONSTR ancestor of the Coq proof
-assistant. CONSTR, then Coq, was designed and implemented in the Formel team,
-joint between the INRIA Rocquencourt laboratory and the École Normale Supérieure
-of Paris, from 1984 onwards.
+This archive contains the sources of the CONSTR ancestor of the Coq
+proof assistant. CONSTR, then Coq, was designed and implemented in the
+Formel team, joint between the INRIA Rocquencourt laboratory and the
+École 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_. Invited paper, EUROCAL85, April 1985, Linz, Austria. Springer Verlag
-LNCS 203, pp. 151-184.
+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_. 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
@@ -57,255 +60,277 @@ 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.
+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.
+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.
+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.
+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.
+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
+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.
+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`.
+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.
+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.
+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.
+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:
+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.
+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…
+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.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:
+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 (INRIA Research Report N°1088, Sept. 1989, published in
-Logic and Computer Science, ed. P.G. Odifreddi, Academic Press, 1990)
+  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 Fω's programs from proofs in the Calculus of Constructions_, by
-Christine Paulin-Mohring (published in POPL'89)
+   Christine Paulin-Mohring,
+- _Extracting Fω'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.
+- _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
+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.
+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 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_. 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.
+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 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.
+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 +