Imported Upstream version 8.6upstream/8.6

11 files changed, 1117 insertions, 332 deletions

diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5
deleted file mode 100644
index ebbc0577..00000000
--- 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 00000000..631fb92c
--- /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.
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index af1120e9..fefcb093 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -30,6 +30,11 @@ HISTORY:
     restricted set of .ml4 (see variable BUILDGRAMMAR).
   - then on the true target asked by the user.
 
+* June 2016 (Pierre Letouzey)
+  The files in grammar/ are now self-contained, we could compile
+  grammar.cma (and q_constr.cmo) directly, no need for a separate
+  subcall to make nor awkward include-failed-and-retry.
+
     
 ---------------------------------------------------------------------------
 
@@ -59,29 +64,14 @@ Cons:
 Makefiles hierachy
 ------------------
 
-Le Makefile a été séparé en plusieurs fichiers :
-
-- Makefile: coquille vide qui lançant Makefile.build sauf pour
-  clean et quelques petites choses ne nécessitant par de calculs
-  de dépendances.
-- Makefile.common : définitions des variables (essentiellement des
-  listes de fichiers)
-- Makefile.build : contient les regles de compilation, ainsi que
-  le "include" des dépendances (restreintes ou non selon la variable
-  BUILDGRAMMAR).
-- Makefile.doc : regles specifiques à la compilation de la documentation.
-
-
-Parallélisation
----------------
+The Makefile is separated in several files :
 
-Il y a actuellement un double appel interne à "make -f Makefile.build",
-d'abord pour construire grammar.cma/q_constr.cmo, puis le reste.
-Cela signifie que ce makefile est un petit peu moins parallélisable
-que strictement possible en théorie: par exemple, certaines choses
-faites lors du second make pourraient être faites en parallèle avec
-le premier. En pratique, ce premier make va suffisemment vite pour
-que cette limitation soit peu gênante.
+- Makefile: wrapper that triggers a call to Makefile.build, except for
+  clean and a few other little things doable without dependency analysis.
+- Makefile.common : variable definitions (mostly lists of files or
+  directories)
+- Makefile.build : contains compilation rules, and the "include" of dependencies
+- Makefile.doc : specific rules for compiling the documentation.
 
 
 FIND_VCS_CLAUSE
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 31d9875a..873adc1b 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -113,15 +113,20 @@ Targets for cleaning various parts:
 
  - docclean: clean documentation
 
-.ml4 files
-----------
+.ml4/.mlp files
+---------------
 
-If a .ml4 file uses a grammar extension from Coq (such as grammar.cma
-or q_constr.cmo), it must contain a line like:
+There is now two kinds of preprocessed files : 
+ - a .mlp do not need grammar.cma (they are in grammar/)
+ - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
+   except coqide_main.ml4 and its specific rule
+
+This classification replaces the old mechanism of declaring the use
+of a grammar extension via a line of the form:
  (*i camlp4deps: "grammar.cma q_constr.cmo" i*)
 
 The use of (*i camlp4use: ... i*) to mention uses of standard
-extension such as IFDEF has been discontinued, the Makefile now
+extension such as IFDEF has also been discontinued, the Makefile now
 always calls camlp4 with pa_macros.cmo and a few others by default.
 
 For debugging a Coq grammar extension, it could be interesting
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2f62be9a..3de938d7 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,5 +1,281 @@
 =========================================
-= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 =
+= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
+=========================================
+
+** Parsing **
+
+Pcoq.parsable now takes an extra optional filename argument so as to
+bind locations to a file name when relevant.
+
+** Files **
+
+To avoid clashes with OCaml's compiler libs, the following files were renamed:
+kernel/closure.ml{,i} -> kernel/cClosure.ml{,i}
+lib/errors.ml{,i} -> lib/cErrors.ml{,i}
+toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i}
+
+All IDE-specific files, including the XML protocol have been moved to ide/
+
+** Reduction functions **
+
+In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX,
+fCOFIX.
+
+We renamed the following functions:
+
+Closure.betadeltaiota -> Closure.all
+Closure.betadeltaiotanolet -> Closure.allnolet
+Reductionops.beta -> Closure.beta
+Reductionops.zeta -> Closure.zeta
+Reductionops.betaiota -> Closure.betaiota
+Reductionops.betaiotazeta -> Closure.betaiotazeta
+Reductionops.delta -> Closure.delta
+Reductionops.betalet -> Closure.betazeta
+Reductionops.betadelta -> Closure.betadeltazeta
+Reductionops.betadeltaiota -> Closure.all
+Reductionops.betadeltaiotanolet -> Closure.allnolet
+Closure.no_red -> Closure.nored
+Reductionops.nored -> Closure.nored
+Reductionops.nf_betadeltaiota -> Reductionops.nf_all
+Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
+Reductionops.whd_betadeltaiota -> Reductionops.whd_all
+Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
+Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
+Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
+Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
+Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
+Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
+Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
+Reductionops.whd_eta -> Reductionops.shrink_eta
+Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
+Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
+
+And removed the following ones:
+
+Reductionops.whd_betaetalet
+Reductionops.whd_betaetalet_stack
+Reductionops.whd_betaetalet_state
+Reductionops.whd_betadeltaeta_stack
+Reductionops.whd_betadeltaeta_state
+Reductionops.whd_betadeltaeta
+Reductionops.whd_betadeltaiotaeta_stack
+Reductionops.whd_betadeltaiotaeta_state
+Reductionops.whd_betadeltaiotaeta
+
+In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and
+FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix.
+
+** Notation_ops **
+
+Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr.
+
+** Logging and Pretty Printing: **
+
+* Printing functions have been removed from `Pp.mli`, which is now a
+  purely pretty-printing interface. Functions affected are:
+
+```` ocaml
+val pp          : std_ppcmds -> unit
+val ppnl        : std_ppcmds -> unit
+val pperr       : std_ppcmds -> unit
+val pperrnl     : std_ppcmds -> unit
+val pperr_flush : unit -> unit
+val pp_flush    : unit -> unit
+val flush_all   : unit -> unit
+val msg         : std_ppcmds -> unit
+val msgnl       : std_ppcmds -> unit
+val msgerr      : std_ppcmds -> unit
+val msgerrnl    : std_ppcmds -> unit
+val message     : string -> unit
+````
+
+  which are no more available. Users of `Pp.pp msg` should now use the
+  proper `Feedback.msg_*` function. Clients also have no control over
+  flushing, the back end takes care of it.
+
+  Also, the `msg_*` functions now take an optional `?loc` parameter
+  for relaying location to the client.
+
+* Feedback related functions and definitions have been moved to the
+  `Feedback` module. `message_level` has been renamed to
+  level. Functions moved from Pp to Feedback are:
+
+```` ocaml
+val set_logger      : logger -> unit
+val std_logger      : logger
+val emacs_logger    : logger
+val feedback_logger : logger
+````
+
+* Changes in the Feedback format/Protocol.
+
+- The `Message` feedback type now carries an optional location, the main
+  payload is encoded using the richpp document format.
+
+- The `ErrorMsg` feedback type is thus unified now with `Message` at
+  level `Error`.
+
+* We now provide several loggers, `log_via_feedback` is removed in
+  favor of `set_logger feedback_logger`. Output functions are:
+
+```` ocaml
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+val msg_error   : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_notice  : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_info    : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_debug   : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+````
+
+  with the `msg_*` functions being just an alias for `logger $Level`.
+
+* The main feedback functions are:
+
+```` ocaml
+val set_feeder : (feedback -> unit) -> unit
+val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+````
+  Note that `feedback` doesn't take two parameters anymore. After
+  refactoring the following function has been removed:
+
+```` ocaml
+val get_id_for_feedback : unit -> edit_or_state_id * route_id
+````
+
+** Kernel API changes **
+
+- The interface of the Context module was changed.
+  Related types and functions were put in separate submodules.
+  The mapping from old identifiers to new identifiers is the following:
+
+    Context.named_declaration            --->  Context.Named.Declaration.t
+    Context.named_list_declaration       --->  Context.NamedList.Declaration.t
+    Context.rel_declaration              --->  Context.Rel.Declaration.t
+    Context.map_named_declaration        --->  Context.Named.Declaration.map_constr
+    Context.map_named_list_declaration   --->  Context.NamedList.Declaration.map
+    Context.map_rel_declaration          --->  Context.Rel.Declaration.map_constr
+    Context.fold_named_declaration       --->  Context.Named.Declaration.fold
+    Context.fold_rel_declaration         --->  Context.Rel.Declaration.fold
+    Context.exists_named_declaration     --->  Context.Named.Declaration.exists
+    Context.exists_rel_declaration       --->  Context.Rel.Declaration.exists
+    Context.for_all_named_declaration    --->  Context.Named.Declaration.for_all
+    Context.for_all_rel_declaration      --->  Context.Rel.Declaration.for_all
+    Context.eq_named_declaration         --->  Context.Named.Declaration.equal
+    Context.eq_rel_declaration           --->  Context.Rel.Declaration.equal
+    Context.named_context                --->  Context.Named.t
+    Context.named_list_context           --->  Context.NamedList.t
+    Context.rel_context                  --->  Context.Rel.t
+    Context.empty_named_context          --->  Context.Named.empty
+    Context.add_named_decl               --->  Context.Named.add
+    Context.vars_of_named_context        --->  Context.Named.to_vars
+    Context.lookup_named                 --->  Context.Named.lookup
+    Context.named_context_length         --->  Context.Named.length
+    Context.named_context_equal          --->  Context.Named.equal
+    Context.fold_named_context           --->  Context.Named.fold_outside
+    Context.fold_named_list_context      --->  Context.NamedList.fold
+    Context.fold_named_context_reverse   --->  Context.Named.fold_inside
+    Context.instance_from_named_context  --->  Context.Named.to_instance
+    Context.extended_rel_list            --->  Context.Rel.to_extended_list
+    Context.extended_rel_vect            --->  Context.Rel.to_extended_vect
+    Context.fold_rel_context             --->  Context.Rel.fold_outside
+    Context.fold_rel_context_reverse     --->  Context.Rel.fold_inside
+    Context.map_rel_context              --->  Context.Rel.map_constr
+    Context.map_named_context            --->  Context.Named.map_constr
+    Context.iter_rel_context             --->  Context.Rel.iter
+    Context.iter_named_context           --->  Context.Named.iter
+    Context.empty_rel_context            --->  Context.Rel.empty
+    Context.add_rel_decl                 --->  Context.Rel.add
+    Context.lookup_rel                   --->  Context.Rel.lookup
+    Context.rel_context_length           --->  Context.Rel.length
+    Context.rel_context_nhyps            --->  Context.Rel.nhyps
+    Context.rel_context_tags             --->  Context.Rel.to_tags
+
+- Originally, rel-context was represented as:
+
+    Context.rel_context = Names.Name.t * Constr.t option * Constr.t
+
+  Now it is represented as:
+
+    Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t
+	                      | LocalDef of Names.Name.t * Constr.t * Constr.t
+ 
+- Originally, named-context was represented as:
+
+    Context.named_context = Names.Id.t * Constr.t option * Constr.t
+
+  Now it is represented as:
+
+    Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t
+	                        | LocalDef of Names.Id.t * Constr.t * Constr.t
+
+- The various EXTEND macros do not handle specially the Coq-defined entries
+  anymore. Instead, they just output a name that have to exist in the scope
+  of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for
+  variables "$name" of type Gram.entry, while the parsing rules of
+  (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will
+  look for variables "wit_$name" of type Genarg.genarg_type. The small DSL
+  for constructing compound entries still works over this scheme. Note that in
+  the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
+  in the parsing rules, so beware of recursive calls.
+  
+  For example, to get "wit_constr" you must "open Constrarg" at the top of the file.
+
+- Evarutil was split in two parts. The new Evardefine file exposes functions
+define_evar_* mostly used internally in the unification engine.
+
+- The Refine module was move out of Proofview.
+
+    Proofview.Refine.* --->  Refine.*
+
+- A statically monotonous evarmap type was introduced in Sigma. Not all the API
+  has been converted, so that the user may want to use compatibility functions
+  Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when
+  needed. Code can be straightforwardly adapted in the following way:
+
+  let (sigma, x1) = ... in
+  ...
+  let (sigma, xn) = ... in
+  (sigma, ans)
+
+  should be turned into:
+
+  open Sigma.Notations
+
+  let Sigma (x1, sigma, p1) = ... in
+  ...
+  let Sigma (xn, sigma, pn) = ... in
+  Sigma (ans, sigma, p1 +> ... +> pn)
+  
+  Examples of `Sigma.Unsafe.of_evar_map` include:
+  
+  Evarutil.new_evar env (Tacmach.project goal) ty   ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty
+
+- The Proofview.Goal.*enter family of functions now takes a polymorphic
+  continuation given as a record as an argument.
+
+  Proofview.Goal.enter begin fun gl -> ... end
+
+  should be turned into
+
+  open Proofview.Notations
+
+  Proofview.Goal.enter { enter = begin fun gl -> ... end }
+  
+- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)`      ---> `Tacinterp.Value.of_constr c`
+- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)`
+- `Pretyping.Termops.mem_named_context`                           ---> `Engine.Termops.mem_named_context_val`
+  (`Global.named_context`                                         ---> `Global.named_context_val`)
+  (`Context.Named.lookup`                                         ---> `Environ.lookup_named_val`)
+
+** Search API **
+
+The main search functions now take a function iterating over the
+results. This allows for clients to use streaming or more economic
+printing.
+
+=========================================
+= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
 =========================================
 
 ** Refactoring : more mli interfaces and simpler grammar.cma **
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index fe896d31..00e7f5c5 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -19,13 +19,6 @@ highparsing :
  Files in parsing/ that cannot be linked too early.
  Contains the grammar rules g_*.ml4
 
-hightactics :
-
- Files in tactics/ that cannot be linked too early.
- These are the .ml4 files that uses the EXTEND possibilities
- provided by grammar.cma, for instance eauto.ml4.
-
-
 Special components
 ------------------
 
diff --git a/dev/doc/drop.txt b/dev/doc/drop.txt
new file mode 100644
index 00000000..3a584741
--- /dev/null
+++ b/dev/doc/drop.txt
@@ -0,0 +1,44 @@
+When you start byte-compiled Coq toplevel:
+
+  rlwrap bin/coqtop.byte
+
+then if you type:
+
+  Drop.
+
+you will decend from Coq toplevel down to Ocaml toplevel.
+So if you want to learn:
+- the current values of some global variables you are interested in
+- or see what happens when you invoke certain functions
+this is the place where you can do that.
+
+When you try to print values belonging to abstract data types:
+
+  # let sigma, env = Lemmas.get_current_context ();;
+  
+  val sigma : Evd.evar_map = <abstr>
+  val env : Environ.env = <abstr>
+
+  # Typeops.infer env (snd (Pretyping.understand_tcc env sigma (Constrintern.intern_constr env (Pcoq.parse_string Pcoq.Constr.lconstr "plus"))));;
+
+  - : Environ.unsafe_judgment = {Environ.uj_val = <abstr>; uj_type = <abstr>}
+
+the printed values are not very helpful.
+
+One way how to deal with that is to load the corresponding printers:
+
+  # #use "dev/include";;
+
+Consequently, the result of:
+
+  # Typeops.infer env (snd (Pretyping.understand_tcc env sigma (Constrintern.intern_constr env (Pcoq.parse_string Pcoq.Constr.lconstr "plus"))));;
+
+will be printed as:
+
+  - : Environ.unsafe_judgment = Nat.add : nat -> nat -> nat
+
+which makes more sense.
+
+To be able to understand the meaning of the data types,
+sometimes the best option is to turn those data types from abstract to concrete
+and look at them without any kind of pretty printing.
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion
index 6274275c..a81f170c 100644
--- a/dev/doc/notes-on-conversion
+++ b/dev/doc/notes-on-conversion
@@ -21,7 +21,7 @@ Notation OMEGA := (ack 4 4).
 
 Definition f (x:nat) := x.
 
-(* Evaluation in tactics can somehow be controled *)
+(* Evaluation in tactics can somehow be controlled *)
 Lemma l1 : OMEGA = OMEGA.
 reflexivity.  (* succeed: identity *)
 Qed.          (* succeed: identity *)
diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt
new file mode 100644
index 00000000..efedbc50
--- /dev/null
+++ b/dev/doc/ocamlbuild.txt
@@ -0,0 +1,30 @@
+Ocamlbuild & Coq
+----------------
+
+A quick note in case someone else gets interested someday in compiling
+Coq via ocamlbuild : such an experimental build system has existed
+in the past (more or less maintained from 2009 to 2013), in addition
+to the official build system via gnu make. But this build via
+ocamlbuild has been severly broken since early 2014 (and don't work
+in 8.5, for instance). This experiment has attracted very limited
+interest from other developers over the years, and has been quite
+cumbersome to maintain, so it is now officially discontinued.
+If you want to have a look at the files of this build system
+(especially myocamlbuild.ml), you can fetch :
+ - my last effort at repairing this build system (up to coqtop.native) :
+   https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair
+ - coq official v8.5 branch (recent but broken)
+ - coq v8.4 branch(less up-to-date, but works).
+
+For the record, the three main drawbacks of this experiments were:
+ - recurrent issues with circularities reported by ocamlbuild
+   (even though make was happy) during the evolution of Coq sources
+ - no proper support of parallel build
+ - quite slow re-traversal of already built things
+See the two corresponding bug reports on Mantis, or
+https://github.com/ocaml/ocamlbuild/issues/52
+
+As an interesting feature, I successfully used this to cross-compile
+Coq 8.4 from linux to win32 via mingw.
+
+Pierre Letouzey, june 2016
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
new file mode 100644
index 00000000..9d2ebf0d
--- /dev/null
+++ b/dev/doc/profiling.txt
@@ -0,0 +1,76 @@
+# How to profile Coq?
+
+I (Pierre-Marie Pédrot) mainly use two OCaml branches to profile Coq, whether I
+want to profile time or memory consumption. AFAIK, this only works for Linux.
+
+## Time
+
+In Coq source folder:
+
+opam switch 4.02.1+fp
+./configure -local -debug
+make
+perf record -g bin/coqtop -compile file.v
+perf report -g fractal,callee --no-children
+
+To profile only part of a file, first load it using
+
+bin/coqtop -l file.v
+
+and plug into the process
+
+perf record -g -p PID
+
+## Memory
+
+You first need a few commits atop trunk for this to work.
+
+git remote add ppedrot https://github.com/ppedrot/coq.git
+git fetch ppedrot
+git checkout ppedrot/allocation-profiling
+git rebase master
+
+Then:
+
+opam switch 4.00.1+alloc-profiling
+./configure -local -debug
+make
+
+Note that linking the coqtop binary takes quite an amount of time with this
+branch, so do not worry too much. There are more recent branches of
+alloc-profiling on mshinwell's repo which can be found at:
+
+https://github.com/mshinwell/opam-repo-dev
+
+### For memory dump:
+
+CAMLRUNPARAM=T,mj bin/coqtop -compile file.v
+
+In another terminal:
+
+pkill -SIGUSR1 $COQTOPPID
+...
+pkill -SIGUSR1 $COQTOPPID
+dev/decode-major-heap.sh heap.$COQTOPPID.$N bin/coqtop
+
+where $COQTOPPID is coqtop pid and $N the index of the call to pkill.
+
+First column is the memory taken by the objects (in words), second one is the
+number of objects and third is the place where the objects where allocated.
+
+### For complete memory graph:
+
+CAMLRUNPARAM=T,gr bin/coqtop -compile file.v
+
+In another terminal:
+
+pkill -SIGUSR1 $COQTOPPID
+...
+pkill -SIGUSR1 $COQTOPPID
+ocaml dev/decodegraph.ml edge.$COQTOPPID.$N bin/coqtop > memory.dot
+dot -Tpdf -o memory.pdf memory.dot
+
+where $COQTOPPID is coqtop pid and $N the index of the call to pkill.
+
+The pdf produced by the last command gives a compact graphical representation of
+the various objects allocated.
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
new file mode 100644
index 00000000..1b016a4e
--- /dev/null
+++ b/dev/doc/setup.txt
@@ -0,0 +1,289 @@
+This document provides detailed guidance on how to:
+- compile Coq
+- take advantage of Merlin in Emacs
+- enable auto-completion for Ocaml source-code
+- use ocamldebug in Emacs for debugging coqtop
+The instructions were tested with Debian 8.3 (Jessie).
+
+The procedure is somewhat tedious, but the final results are (still) worth the effort.
+
+How to compile Coq
+------------------
+
+Getting build dependencies:
+
+  sudo apt-get install make opam git mercurial darcs
+  opam init --comp 4.02.3
+  # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files.
+  
+  source ~/.bashrc
+  
+  # needed if you want to build "coqtop" target
+  opam install camlp5
+  
+  # needed if you want to build "coqide" target
+  sudo apt-get install liblablgtksourceview2-ocaml-dev libgtk2.0-dev libgtksourceview2.0-dev
+  opam install lablgtk
+  
+  # needed if you want to build "doc" target
+  sudo apt-get install texlive-latex-recommended texlive-fonts-extra texlive-math-extra \
+                       hevea texlive-latex-extra latex-xcolor
+
+Cloning Coq:
+
+  # Go to the directory where you want to clone Coq's source-code. E.g.:
+  cd ~/git
+
+  git clone https://github.com/coq/coq.git
+
+Building coqtop:
+
+  cd ~/git/coq
+  git checkout trunk
+  make distclean
+  ./configure -annotate -with-doc no -local -debug -usecamlp5
+  make clean
+  make -j4 coqide printers
+
+The "-annotate" option is essential when one wants to use Merlin.
+
+The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install
+
+The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary.
+
+Then check if
+- bin/coqtop
+- bin/coqide
+behave as expected.
+
+
+A note about rlwrap
+-------------------
+
+Running "coqtop" under "rlwrap" is possible, but there is a catch. If you try:
+
+  cd ~/git/coq
+  rlwrap bin/coqtop
+
+you will get an error:
+
+  rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory
+
+This is a known issue:
+
+  https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=779692
+
+It was fixed upstream in version 0.42, and in a Debian package that, at the time of writing, is not part of Debian stable/testing/sid archives but only of Debian experimental.
+
+  https://packages.debian.org/experimental/rlwrap
+
+The quick solution is to grab it from there, since it installs fine on Debian stable (jessie).
+
+  cd /tmp
+  wget  http://ftp.us.debian.org/debian/pool/main/r/rlwrap/rlwrap_0.42-1_amd64.deb
+  sudo dpkg -i rlwrap_0.42-1_amd64.deb
+
+After that, "rlwrap" works fine with "coqtop".
+
+
+How to install and configure Merlin (for Emacs)
+-----------------------------------------------
+
+  sudo apt-get install emacs
+
+  opam install tuareg
+  # Follow the advice displayed at the end as how to update your ~/.emacs file.
+  
+  opam install merlin
+  # Follow the advice displayed at the end as how to update your ~/.emacs file.
+
+Then add this:
+
+  (push "~/.opam/4.02.3/share/emacs/site-lisp" load-path)     ; directory containing merlin.el
+  (setq merlin-command "~/.opam/4.02.3/bin/ocamlmerlin")      ; needed only if ocamlmerlin not already in your PATH
+  (autoload 'merlin-mode "merlin" "Merlin mode" t)
+  (add-hook 'tuareg-mode-hook 'merlin-mode)
+  (add-hook 'caml-mode-hook 'merlin-mode)
+  (load "~/.opam/4.02.3/share/emacs/site-lisp/tuareg-site-file")
+  
+  ;; Do not use TABs. These confuse Merlin.
+  (setq-default indent-tabs-mode nil)
+
+to your ~/.emacs file.
+
+Further Emacs configuration when we start it for the first time.
+
+Try to open some *.ml file in Emacs, e.g.:
+
+  cd ~/git/coq
+  emacs toplevel/coqtop.ml &
+
+Emacs display the following strange message:
+
+  The local variables list in ~/git/coq
+  contains values that may be safe (*).
+
+  Do you want to apply it?
+
+Just press "!", i.e. "apply the local variable list, and permanently mark these values (\*) as safe."
+
+Emacs then shows two windows:
+- one window that shows the contents of the "toplevel/coqtop.ml" file
+- and the other window that shows greetings for new Emacs users.
+
+If you do not want to see the second window next time you start Emacs, just check "Never show it again" and click on "Dismiss this startup screen."
+
+The default key-bindings are described here:
+
+  https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch
+
+If you want, you can customize them by replacing the following lines:
+
+  (define-key merlin-map (kbd "C-c C-x") 'merlin-error-next)
+  (define-key merlin-map (kbd "C-c C-l") 'merlin-locate)
+  (define-key merlin-map (kbd "C-c &") 'merlin-pop-stack)
+  (define-key merlin-map (kbd "C-c C-t") 'merlin-type-enclosing)
+
+in the file "~/.opam/4.02.3/share/emacs/site-lisp/merlin.el" with what you want.
+In the text below we assume that you changed the origin key-bindings in the following way:
+
+  (define-key merlin-map (kbd "C-n") 'merlin-error-next)
+  (define-key merlin-map (kbd "C-l") 'merlin-locate)
+  (define-key merlin-map (kbd "C-b") 'merlin-pop-stack)
+  (define-key merlin-map (kbd "C-t") 'merlin-type-enclosing)
+
+Now, when you press <Ctrl+L>, Merlin will show the definition of the symbol in a separate window.
+If you prefer to jump to the definition within the same window, do this:
+
+  <Alt+X> customize-group <ENTER> merlin <ENTER>
+
+    Merlin Locate In New Window
+
+      Value Menu
+
+        Never Open In New Window
+
+      State
+
+        Set For Future Sessions
+
+Testing (Merlin):
+
+  cd ~/git/coq
+  emacs toplevel/coqtop.ml &
+
+Go to the end of the file where you will see the "start" function.
+
+Go to a line where "init_toplevel" function is called.
+
+If you want to jump to the position where that function or datatype under the cursor is defined, press <Ctrl+L>.
+
+If you want to jump back, type: <Ctrl+B>
+
+If you want to learn the type of the value at current cursor's position, type: <Ctrl+T>
+
+
+Enabling auto-completion in emacs
+---------------------------------
+
+In Emacs, type: <Alt+M> list-packages <ENTER>
+
+In the list that is displayed, click on "company".
+
+A new window appears where just click on "Install" and then answer "Yes".
+
+These lines:
+
+  (package-initialize)
+  (require 'company)
+  ; Make company aware of merlin
+  (add-to-list 'company-backends 'merlin-company-backend)
+  ; Enable company on merlin managed buffers
+  (add-hook 'merlin-mode-hook 'company-mode)
+  (global-set-key [C-tab] 'company-complete)
+
+then need to be added to your "~/.emacs" file.
+
+Next time when you start emacs and partially type some identifier,
+emacs will offer the corresponding completions.
+Auto-completion can also be manually invoked by typing <Ctrl+TAB>.
+Description of various other shortcuts is here.
+
+  http://company-mode.github.io/
+
+
+Getting along with ocamldebug
+-----------------------------
+
+The default ocamldebug key-bindings are described here.
+
+  http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec369
+
+If you want, you can customize them by putting the following commands:
+
+  (global-set-key (kbd "<f5>") 'ocamldebug-break)
+  (global-set-key (kbd "<f6>") 'ocamldebug-run)
+  (global-set-key (kbd "<f7>") 'ocamldebug-next)
+  (global-set-key (kbd "<f8>") 'ocamldebug-step)
+  (global-set-key (kbd "<f9>") 'ocamldebug-finish)
+  (global-set-key (kbd "<f10>") 'ocamldebug-print)
+  (global-set-key (kbd "<f12>") 'camldebug)
+
+to your "~/.emacs" file.
+
+Let us try whether ocamldebug in Emacs works for us.
+(If necessary, re-)compile coqtop:
+
+  cd ~/git/coq
+  make -j4 coqide printers
+
+open Emacs:
+
+  emacs toplevel/coqtop.ml &
+
+and type:
+
+  <F12> ../bin/coqtop.byte <ENTER> ../dev/ocamldebug-coq <ENTER>
+
+As a result, a new window is open at the bottom where you should see:
+
+  (ocd)
+
+i.e. an ocamldebug shell.
+
+  1. Switch to the window that contains the "coqtop.ml" file.
+  2. Go to the end of the file.
+  3. Find the definition of the "start" function.
+  4. Go to the "let" keyword that is at the beginning of the first line.
+  5. By pressing <F5> you set a breakpoint to the cursor's position.
+  6. By pressing <F6> you start the bin/coqtop process.
+  7. Then you can:
+     - step over function calls: <F7>
+     - step into function calls: <F8>
+     - or finish execution of the current function until it returns: <F9>.
+
+Other ocamldebug commands, can be typed to the window that holds the ocamldebug shell.
+
+The points at which the execution of Ocaml program can stop are defined here:
+
+  http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec350
+
+
+Installing printers to ocamldebug
+---------------------------------
+
+There is a pretty comprehensive set of printers defined for many common data types.
+You can load them by switching to the window holding the "ocamldebug" shell and typing:
+
+  (ocd) source "../dev/db"
+
+
+Some of the functions were you might want to set a breakpoint and see what happens next
+---------------------------------------------------------------------------------------
+
+- Coqtop.start : This function is called by the code produced by "coqmktop".
+- Coqtop.parse_args : This function is responsible for parsing command-line arguments.
+- Coqloop.loop : This function implements the read-eval-print loop.
+- Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\
+                         It dispatches the control to specific functions handling different Vernacular command.
+- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command.