From d974365ef5928048edb87af218f6105ae454c3b6 Mon Sep 17 00:00:00 2001
From: Gabriel Scherer
Date: Thu, 25 Jun 2015 10:48:03 +0200
Subject: dev/tool/anomaly-traces-parser.el

An .emacs-ready elisp snippet to parse location of Anomaly backtraces
and jump to them conveniently from the Emacs *compilation* output.
---
 dev/README                         |  3 +++
 dev/tools/anomaly-traces-parser.el | 28 ++++++++++++++++++++++++++++
 2 files changed, 31 insertions(+)
 create mode 100644 dev/tools/anomaly-traces-parser.el

(limited to 'dev')

diff --git a/dev/README b/dev/README
index 5edf64c8f2..814f609576 100644
--- a/dev/README
+++ b/dev/README
@@ -45,3 +45,6 @@ Makefile.subdir: makefile dedicated to intensive work in a given subdirectory
 Makefile.devel: utilities to automatically launch coq in various states
 Makefile.common: used by other Makefiles
 objects.el: various development utilities at emacs level
+anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse
+  location of Anomaly backtraces and jump to them conveniently from
+  the Emacs *compilation* output.
diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el
new file mode 100644
index 0000000000..68f54266f9
--- /dev/null
+++ b/dev/tools/anomaly-traces-parser.el
@@ -0,0 +1,28 @@
+;; This Elisp snippet adds a regexp parser for the format of Anomaly
+;; backtraces (coqc -bt ...), to the error parser of the Compilation
+;; mode (C-c C-c: "Compile command: ..."). Once the
+;; coq-change-error-alist-for-backtraces function has run, file
+;; locations in traces are recognized and can be jumped from easily
+;; from the *compilation* buffer.
+
+;; You can just copy everything below to your .emacs and this will be
+;; enabled from any compilation command launched from an OCaml file.
+
+(defun coq-change-error-alist-for-backtraces ()
+  "Hook to change the compilation-error-regexp-alist variable, to
+   search the coq backtraces for error locations"
+  (interactive)
+  (add-to-list
+   'compilation-error-regexp-alist-alist
+   '(coq-backtrace
+     "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\
+      lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\
+      \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)"
+     2 (3 . 4) (5 . 6)))
+  (add-to-list 'compilation-error-regexp-alist 'coq-backtrace))
+
+;; this Anomaly parser should be available when one is hacking
+;; on the *OCaml* code of Coq (adding bugs), so we enable it
+;; through the OCaml mode hooks.
+(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces)
+(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces)
-- 
cgit v1.2.3


From 5a0da4d8ea9b590e30ba9b194789b348be6bbc4f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 17 Sep 2015 07:49:19 +0200
Subject: Fix Windows installer.

The theories/ directory contains no cmi/cmxs files when native_compute is
disabled, so do not try to ship them.
---
 dev/nsis/coq.nsi | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index 5b421e49dd..676490510c 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -95,8 +95,8 @@ Section "Coq" Sec1
   File /r ${COQ_SRC_PATH}\theories\*.vo
   File /r ${COQ_SRC_PATH}\theories\*.v
   File /r ${COQ_SRC_PATH}\theories\*.glob
-  File /r ${COQ_SRC_PATH}\theories\*.cmi
-  File /r ${COQ_SRC_PATH}\theories\*.cmxs
+  ; File /r ${COQ_SRC_PATH}\theories\*.cmi
+  ; File /r ${COQ_SRC_PATH}\theories\*.cmxs
   SetOutPath "$INSTDIR\lib\plugins"
   File /r ${COQ_SRC_PATH}\plugins\*.vo
   File /r ${COQ_SRC_PATH}\plugins\*.v
-- 
cgit v1.2.3


From 8bba34395e520ac606fc3efd0a875699fe968e69 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 00:08:35 +0200
Subject: Better debug printers for module paths.

Now distinguishes between bound modules (Top#X) and submodules (Top.X).

Could be useful for the regular printer as well (e.g. in error messages), but I
don't know what the compatibility constraints are, so leaving it as it is for
now.
---
 dev/db              | 1 +
 dev/top_printers.ml | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/db b/dev/db
index f259b50eb3..ece22b3f44 100644
--- a/dev/db
+++ b/dev/db
@@ -13,6 +13,7 @@ install_printer Top_printers.ppexistentialset
 install_printer Top_printers.ppintset
 install_printer Top_printers.pplab
 install_printer Top_printers.ppdir
+install_printer Top_printers.ppmbid
 install_printer Top_printers.ppmp
 install_printer Top_printers.ppkn
 install_printer Top_printers.ppcon
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9f2e1b09e..0900bb0962 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -40,10 +40,10 @@ let ppid id = pp (pr_id id)
 let pplab l = pp (pr_lab l)
 let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
 let ppdir dir = pp (pr_dirpath dir)
-let ppmp mp = pp(str (string_of_mp mp))
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
 let ppcon con = pp(debug_pr_con con)
 let ppproj con = pp(debug_pr_con (Projection.constant con))
-let ppkn kn = pp(pr_kn kn)
+let ppkn kn = pp(str (KerName.to_string kn))
 let ppmind kn = pp(debug_pr_mind kn)
 let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
 let ppsp sp = pp(pr_path sp)
-- 
cgit v1.2.3


From 0d923ee82bfed8d33d677dafb4b8defa18e4fdd1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 22 Sep 2015 20:14:59 +0200
Subject: Univs: More info for developers.

---
 dev/doc/univpoly.txt | 48 ++++++++++++++++++++++++++++++++++++------------
 1 file changed, 36 insertions(+), 12 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index 4c89af01db..bad2ae36eb 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -1,5 +1,5 @@
-Notes on universe polymorphism and primitive projections, M. Sozeau - WIP 
-=========================================================================
+Notes on universe polymorphism and primitive projections, M. Sozeau
+===================================================================
 
 The new implementation of universe polymorphism and primitive
 projections introduces a few changes to the API of Coq. First and
@@ -46,15 +46,16 @@ universes and constraints to the global universe context when it is put
 in the environment. No other universes than the global ones and the
 declared local ones are needed to check a declaration, hence the kernel
 does not produce any constraints anymore, apart from module
-subtyping.... There are hance two conversion functions now: check_conv
-and infer_conv: the former just checks the definition in the current env
+subtyping.... There are hence two conversion functions now: [check_conv]
+and [infer_conv]: the former just checks the definition in the current env
 (in which we usually push_universe_context of the associated context),
-and infer_conv which produces constraints that were not implied by the
+and [infer_conv] which produces constraints that were not implied by the
 ambient constraints. Ideally, that one could be put out of the kernel,
-but again, module subtyping needs it. 
+but currently module subtyping needs it. 
 
  Inference of universes is now done during refinement, and the evar_map
-carries the incrementally built universe context. [Evd.conversion] is a
+carries the incrementally built universe context, starting from the
+global universe constraints (see [Evd.from_env]). [Evd.conversion] is a
 wrapper around [infer_conv] that will do the bookkeeping for you, it
 uses [evar_conv_x]. There is a universe substitution being built
 incrementally according to the constraints, so one should normalize at
@@ -72,7 +73,7 @@ val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> ta
 Is the way to make a constr out of a global reference in the new API.
 If they constr is polymorphic, it will add the necessary constraints to
 the evar_map. Even if a constr is not polymorphic, we have to take care
-of keeping track of it's universes. Typically, using:
+of keeping track of its universes. Typically, using:
 
   mkApp (coq_id_function, [| A; a |]) 
 
@@ -84,8 +85,8 @@ produce the right constraints and put them in the evar_map. Of course in
 some cases you might now from an invariant that no new constraint would
 be produced and get rid of it. Anyway the kernel will tell you if you
 forgot some. As a temporary way out, [Universes.constr_of_global] allows
-you to make a constr from any non-polymorphic constant, but it might
-forget constraints.
+you to make a constr from any non-polymorphic constant, but it will fail
+on polymorphic ones.
 
 Other than that, unification (w_unify and evarconv) now take account of universes and
 produce only well-typed evar_maps.
@@ -157,6 +158,30 @@ this is the only solution I found. In the case of global_references
 only, it's just a matter of using [Evd.fresh_global] /
 [pf_constr_of_global] to let the system take care of universes.
 
+
+The universe graph
+==================
+
+To accomodate universe polymorphic definitions, the graph structure in
+kernel/univ.ml was modified. The new API forces every universe to be
+declared before it is mentionned in any constraint. This forces to
+declare every universe to be >= Set or > Set. Every universe variable
+introduced during elaboration is >= Set. Every _global_ universe is now
+declared explicitely > Set, _after_ typechecking the definition. In
+polymorphic definitions Type@{i} ranges over Set and any other universe
+j. However, at instantiation time for polymorphic references, one can
+try to instantiate a universe parameter with Prop as well, if the
+instantiated constraints allow it. The graph invariants ensure that
+no universe i can be set lower than Set, so the chain of universes
+always bottoms down at Prop < Set.
+
+Modules
+=======
+
+One has to think of universes in modules as being globally declared, so
+when including a module (type) which declares a type i (e.g. through a
+parameter), we get back a copy of i and not some fresh universe.
+
 Projections
 ===========
 
@@ -208,8 +233,7 @@ constants left (the most common case). E.g. Ring with Set Universe
 Polymorphism and Set Primitive Projections work (at least it did at some
 point, I didn't recheck yet).  
 
-- [native_compute] is untested: it should deal with primitive
-projections right but not universes.
+- [native_compute] works with universes and projections.
 
 
 Incompatibilities
-- 
cgit v1.2.3


From 6e1c88226eb2ab188a1aaaf9a31667967c85fc65 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Oct 2015 16:32:20 +0200
Subject: Update the history of versions with recent versions.

---
 dev/doc/versions-history.tex | 50 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 9892a4419f..fab6a37ef4 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -265,7 +265,17 @@ Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\
   & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\
 
 Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\
+\end{tabular}
 
+\medskip
+\bigskip
+
+\centerline{V- New concrete syntax}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
 Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\
 
 Coq V8.0pl1& released 18 July 2004\\
@@ -307,6 +317,46 @@ Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \fea
 
 & & a first package released on
 February 11 was incomplete\\
+Coq V8.2pl1& released 4 July 2009 & \\
+Coq V8.2pl2& released 29 June 2010 & \\
+\end{tabular}
+
+\medskip
+\bigskip
+
+\newpage
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+Coq V8.3 beta & released 16 February 2010 & \feature{MSets library} [13-10-2009] \\
+Coq V8.3 & released 14 October 2010 & \feature{nsatz} [3-6-2010] \\
+Coq V8.3pl1& released 23 December 2010 & \\
+Coq V8.3pl2& released 19 April 2011 & \\
+Coq V8.3pl3& released 19 December 2011 & \\
+Coq V8.3pl3& released 26 March 2012 & \\
+Coq V8.3pl5& released 28 September 2012 & \\
+Coq V8.4 beta & released 27 December 2011 &  \feature{modular arithmetic library} [2010-2012]\\
+&& \feature{vector library} [10-12-2010]\\
+&& \feature{structured scripts} [22-4-2010]\\
+&& \feature{eta-conversion} [20-9-2010]\\
+&& \feature{new proof engine available} [10-12-2010]\\
+Coq V8.4 beta2 & released 21 May 2012 & \\
+Coq V8.4 & released 12 August 2012 &\\
+Coq V8.4pl1& released 22 December 2012 & \\
+Coq V8.4pl2& released 4 April 2013 & \\
+Coq V8.4pl3& released 21 December 2013 & \\
+Coq V8.4pl4& released 24 April 2014 & \\
+Coq V8.4pl5& released 22 October 2014 & \\
+Coq V8.4pl6& released 9 April 2015 & \\
+
+Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\
+&& \feature{asynchonous evaluation} [8-8-2013]\\
+&& \feature{new proof engine deployed} [2-11-2013]\\
+&& \feature{universe polymorphism} [6-5-2014]\\
+&& \feature{primitive projections} [6-5-2014]\\
+
+Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\
+
 \end{tabular}
 
 \medskip
-- 
cgit v1.2.3


From beedccef9ddc8633c705d7c5ee2f1bbbb3ec8a47 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Oct 2015 17:43:32 +0200
Subject: Updating versions history with data from Gérard.

Adding Gérard's history file about V1-V5 versions.
---
 dev/doc/README-V1-V5         | 293 +++++++++++++++++++++++++++++++++++++++++++
 dev/doc/versions-history.tex |  59 ++++++---
 2 files changed, 333 insertions(+), 19 deletions(-)
 create mode 100644 dev/doc/README-V1-V5

(limited to 'dev')

diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5
new file mode 100644
index 0000000000..2ca62e3d74
--- /dev/null
+++ b/dev/doc/README-V1-V5
@@ -0,0 +1,293 @@
+
+                 Notes on the prehistory of Coq
+
+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 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/versions-history.tex b/dev/doc/versions-history.tex
index fab6a37ef4..1b1d3500a4 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -10,55 +10,76 @@
 
 \begin{center}
 \begin{huge}
-An history of Coq versions
+A history of Coq versions
 \end{huge}
 \end{center}
 \bigskip
 
 \centerline{\large 1984-1989: The Calculus of Constructions}
+
+\bigskip
+\centerline{\large (see README.V1-V5 for details)}
 \mbox{}\\
 \mbox{}\\
 \begin{tabular}{l|l|l}
 version & date & comments \\
 \hline
-CoC V1.10& mention of dates from 6 December & implementation language is Caml\\
-         & 1984 to 13 February 1985 \\
 
-CoC V1.11& mention of dates from 6 December\\
-         & 1984 to 19 February 1985\\
+CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\
+         & 1984 to 13 February 1985 & \feature{of Constructions}, implementation  \\
+         & frozen 22 December 1984 & language is a predecessor of CAML\\
+
+CONSTR V1.11& mention of dates from 6 December\\
+         & 1984 to 19 February 1985 (freeze date) &\\
+
+CoC V2.8& dated 16 December 1985 (freeze date)\\
 
-CoC V2.13& dated 16 December 1985\\
+CoC V2.9& & \feature{cumulative hierarchy of universes}\\
 
-CoC V2.13& dated 25 June 1986\\
+CoC V2.13& dated 25 June 1986 (freeze date)\\
 
-CoC V3.1& dated 20 November 1986 & \feature{auto}\\
+CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\
+  & dated 20 November 1986 & implementation language now named CAML\\
 
 CoC V3.2& dated 27 November 1986\\
 
-CoC V3.3 and V3.4& dated 1 January 1987 & creation of a directory for examples\\
+CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\
 
-CoC V4.1& dated 24 July 1987\\
+CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\
+
+CoC V4.1& dated 24 July 1987 (freeze date)\\
 
 CoC V4.2& dated 10 September 1987\\
 
-CoC V4.3& dated 15 September 1987\\
+CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\
+  & frozen November 1987 & \feature{section mechanism}\\
+  & & \feature{logical vs computational content (sorte Spec)}\\
+  & & \feature{LCF engine}\\
+
+CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\
+  & frozen March 1988\\
 
-CoC V4.4& dated 27 January 1988\\
+CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\
+  & demonstrated in June 1988\\
 
-CoC V4.5 and V4.5.5& dated 15 March 1988\\
+CoC V4.6& dated 1 September 1988 & start of LEGO fork\\
 
-CoC V4.6 and V4.7& dated 1 September 1988\\
+CoC V4.7& started 6 September 1988 \\
 
-CoC V4.8& dated 1 December 1988\\
+CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\
 
-CoC V4.8.5& dated 1 February 1989\\
+CoC V4.8.5& dated 1 February 1989 & \\
 
-CoC V4.9& dated 1 March 1989\\
+CoC V4.9& dated 1 March 1989 (release date)\\
 
-CoC V4.10 and 4.10.1& dated 1 May 1989 & first public release - in English\\
+CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\
 \end{tabular}
 
 \bigskip
+
+\noindent Note: CoC above stands as an abbreviation for {\em Calculus of
+  Constructions}, official name of the system.
+\bigskip
 \bigskip
 
 \newpage
@@ -80,7 +101,7 @@ Coq V5.2 & log dated 4 October 1990 & internal use \\
 
 Coq V5.3 & log dated 12 October 1990 & internal use \\
 
-Coq V5.4 & headers dated 24 October 1990 & internal use, \feature{extraction} (version 1) [3-12-90]\\
+Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\
 
 Coq V5.5 & started 6 December 1990 & internal use \\
 
-- 
cgit v1.2.3


From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Oct 2015 19:09:10 +0200
Subject: Splitting kernel universe code in two modules.

1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
---
 dev/printers.mllib  | 1 +
 dev/top_printers.ml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 07b48ed573..f19edf1c80 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -55,6 +55,7 @@ Monad
 
 Names
 Univ
+UGraph
 Esubst
 Uint31
 Sorts
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0900bb0962..1d3d711ac7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -221,7 +221,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppuniverses u = pp (Univ.pr_universes Level.pr u)
+let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
 
-- 
cgit v1.2.3


From 7c82718f18afa3b317873f756a8801774ef64061 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:19:20 +0200
Subject: Minor typo in universe polymorphism doc.

---
 dev/doc/univpoly.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index bad2ae36eb..9e243eead5 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -82,7 +82,7 @@ show that A's type is in cumululativity relation with id's type
 argument, incurring a universe constraint. To do this, one can simply
 call Typing.resolve_evars env evdref c which will do some infer_conv to
 produce the right constraints and put them in the evar_map. Of course in
-some cases you might now from an invariant that no new constraint would
+some cases you might know from an invariant that no new constraint would
 be produced and get rid of it. Anyway the kernel will tell you if you
 forgot some. As a temporary way out, [Universes.constr_of_global] allows
 you to make a constr from any non-polymorphic constant, but it will fail
-- 
cgit v1.2.3


From c47b205206d832430fa80a3386be80149e281d33 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:04:56 +0200
Subject: Code cleaning in VM (with Benjamin).

Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
---
 dev/vm_printers.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 3d688011c2..802b0f9d80 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -61,7 +61,6 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Aiddef(idk,_) -> print_string "&";print_idkey idk
   | Aind((sp,i),_) ->  print_string "Ind(";
       print_string (string_of_mind sp);
       print_string ","; print_int i;
-- 
cgit v1.2.3


From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 13 Oct 2015 18:30:47 +0200
Subject: Fix some typos.

---
 dev/doc/univpoly.txt      | 2 +-
 dev/v8-syntax/memo-v8.tex | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index 9e243eead5..6a69c57934 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -167,7 +167,7 @@ kernel/univ.ml was modified. The new API forces every universe to be
 declared before it is mentionned in any constraint. This forces to
 declare every universe to be >= Set or > Set. Every universe variable
 introduced during elaboration is >= Set. Every _global_ universe is now
-declared explicitely > Set, _after_ typechecking the definition. In
+declared explicitly > Set, _after_ typechecking the definition. In
 polymorphic definitions Type@{i} ranges over Set and any other universe
 j. However, at instantiation time for polymorphic references, one can
 try to instantiate a universe parameter with Prop as well, if the
diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex
index 8d116de26f..ae4b569b36 100644
--- a/dev/v8-syntax/memo-v8.tex
+++ b/dev/v8-syntax/memo-v8.tex
@@ -253,7 +253,7 @@ became \TERM{context}. Syntax is unified with subterm matching.
 \subsection{Occurrences}
 
 To avoid ambiguity between a numeric literal and the optionnal
-occurence numbers of this term, the occurence numbers are put after
+occurrence numbers of this term, the occurrence numbers are put after
 the term itself. This applies to tactic \TERM{pattern} and also
 \TERM{unfold}
 \begin{transbox}
-- 
cgit v1.2.3


From a895b2c0caf8ec9c0deb04b8dea890283bd7329d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Oct 2015 12:16:36 +0200
Subject: Fixing  perfomance issue of auto hints induced by universes.

Instead of brutally merging the whole evarmap coming from the clenv,
we remember the context associated to the hint and we only merge that tiny
part of constraints. We need to be careful for polymorphic hints though,
as we have to refresh them beforehand.
---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9f2e1b09e..059c812ad5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -165,7 +165,7 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
+let ppevm evd = pp(Evd.pr_evar_universe_context (Evd.evar_universe_context evd))
 let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
-- 
cgit v1.2.3


From 1d6c4f135d42a008b21d86d8ecd8b329405d8d7c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Oct 2015 18:51:47 +0200
Subject: Reverting modifications in dev/top_printers pushed mistakenly.

---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 059c812ad5..f9f2e1b09e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -165,7 +165,7 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(Evd.pr_evar_universe_context (Evd.evar_universe_context evd))
+let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
 let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
-- 
cgit v1.2.3


From 68863acca9abf4490c651df889721ef7f6a4d375 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Oct 2015 15:32:03 +0200
Subject: Dedicated file for universe unification context manipulation.

This allows to remove a lot of independent code from Evd which was put
into the UState module. The API is not perfect yet, but this is a first
pass. Names of data structures should be thought about too because they
are way too similar.
---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index f19edf1c80..b81fe151f7 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -117,6 +117,7 @@ Miscops
 Universes
 Termops
 Namegen
+UState
 Evd
 Glob_ops
 Redops
-- 
cgit v1.2.3


From 7cfb1c359faf13cd55bd92cba21fb00ca8d2d0d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Sep 2015 19:08:11 +0200
Subject: Adding a notion of monotonous evarmap.

---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index b81fe151f7..de43efa670 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -119,6 +119,7 @@ Termops
 Namegen
 UState
 Evd
+Sigma
 Glob_ops
 Redops
 Reductionops
-- 
cgit v1.2.3


From 010775eba60ea89645792b48a0686ff15c4ebcb5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 25 Oct 2015 18:43:32 +0100
Subject: Pcoq entries are given a proper module.

Entries defined in the Pcoq AST of symbols must be marshallable, because they
are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as
they contain functional values. This is why the Pcoq module used a pair
[string * string] to describe entries. It is obviously type-unsafe, so
we define a new abstract type in its own module. There is a little issue
though, which is that our entries and CAMLP4/5 entries must be kept
synchronized through an association table. The Pcoq module tries to
maintain this invariant.
---
 dev/printers.mllib  | 1 +
 dev/top_printers.ml | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index de43efa670..1a2819feb2 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -191,6 +191,7 @@ Pfedit
 Tactic_debug
 Decl_mode
 Ppconstr
+Entry
 Pcoq
 Printer
 Pptactic
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 1d3d711ac7..7b807a343a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -519,7 +519,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
+        (Loc.ghost,ConstrArgType,Aentry (Entry.unsafe_of_name ("constr","constr")),
 	 Some (Names.Id.of_string "c"))]
 
 let _ =
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
+        (Loc.ghost,ConstrArgType,Aentry (Entry.unsafe_of_name ("constr","constr")),
 	 Some (Names.Id.of_string "c"))]
 
 (* Setting printer of unbound global reference *)
-- 
cgit v1.2.3


From 72bed859fb8d037044abd8a1518661c52502f7be Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 27 Oct 2015 11:44:58 +0100
Subject: Type-safe Egramml.grammar_prod_item.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7b807a343a..b3b1ae0e91 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -519,7 +519,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,ConstrArgType,Aentry (Entry.unsafe_of_name ("constr","constr")),
+        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")),
 	 Some (Names.Id.of_string "c"))]
 
 let _ =
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,ConstrArgType,Aentry (Entry.unsafe_of_name ("constr","constr")),
+        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")),
 	 Some (Names.Id.of_string "c"))]
 
 (* Setting printer of unbound global reference *)
-- 
cgit v1.2.3


From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Sat, 17 Oct 2015 21:40:49 -0700
Subject: Adds support for the virtual machine to perform reduction of universe
 polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
---
 dev/vm_printers.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 802b0f9d80..272df7b421 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -13,7 +13,7 @@ let ppripos (ri,pos) =
 	("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
-  | Reloc_getglobal (kn,_) ->
+  | Reloc_getglobal kn ->
       print_string ("getglob "^(string_of_con kn)^"\n"));
    print_flush ()
 
@@ -30,7 +30,7 @@ let ppsort = function
 
 let print_idkey idk =
   match idk with
-  | ConstKey (sp,_) ->
+  | ConstKey sp ->
       print_string "Cons(";
       print_string (string_of_con sp);
       print_string ")"
@@ -61,7 +61,8 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Aind((sp,i),_) ->  print_string "Ind(";
+  | Atype u -> print_string "Type(...)"
+  | Aind(sp,i) ->  print_string "Ind(";
       print_string (string_of_mind sp);
       print_string ","; print_int i;
       print_string ")"
-- 
cgit v1.2.3


From 4f8a9d10123bd8aa4d17853a7248d3b3fe8a3625 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 28 Oct 2015 11:16:24 +0100
Subject: Refine Gregory Malecha's patch on VM and universe polymorphism.

- Universes are now represented in the VM by a structured constant containing the
  global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
  a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
  constructor arguments, which has to be prevented.
  Was showing up for instance when evaluating [cons _ list (nil _)] with
  a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
  Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.

Patch written with Benjamin Grégoire.
---
 dev/vm_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 272df7b421..1c501df808 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -79,6 +79,7 @@ and ppwhd whd =
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s
+  | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl)
 
 and ppvblock b =
   open_hbox();
-- 
cgit v1.2.3


From 654b69cbeb55a0cab3c2328d73355ad2510d1a85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Oct 2015 14:21:25 +0100
Subject: Fixing another instance of bug #3267 in eauto, this time in the
 presence of hints modifying the context and of a "using" clause.

Incidentally opening Hints by default in debugger.
---
 dev/base_include | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index d58b6ad13c..dac1f6093c 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -148,6 +148,7 @@ open Tactic_debug
 open Decl_proof_instr
 open Decl_mode
 
+open Hints
 open Auto
 open Autorewrite
 open Contradiction
-- 
cgit v1.2.3


From 5357b9849bd6eb0be4f8d60b4e1c091ad5167932 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 5 Nov 2015 19:43:44 +0100
Subject: Prehistory of Coq: asciidoc conversion.

Formatting markup + typography.
---
 dev/doc/README-V1-V5          | 293 ---------------------------------------
 dev/doc/README-V1-V5.asciidoc | 312 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 312 insertions(+), 293 deletions(-)
 delete mode 100644 dev/doc/README-V1-V5
 create mode 100644 dev/doc/README-V1-V5.asciidoc

(limited to 'dev')

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


From e82fc7cb4104d28619448bde374afde7e32f3dc2 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 6 Nov 2015 09:15:47 +0100
Subject: Prehistory of Coq: various corrections on English.

---
 dev/doc/README-V1-V5.asciidoc | 31 ++++++++++++++++---------------
 1 file changed, 16 insertions(+), 15 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc
index f6ee27d486..43971ba553 100644
--- a/dev/doc/README-V1-V5.asciidoc
+++ b/dev/doc/README-V1-V5.asciidoc
@@ -25,10 +25,10 @@ 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
+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.
 
@@ -47,10 +47,11 @@ Th. Coquand, G. Huet. _Constructions: A Higher Order Proof System for Mechanizin
 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
+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
@@ -185,7 +186,7 @@ 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
+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.
 
@@ -209,9 +210,9 @@ 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…
+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.
@@ -238,7 +239,7 @@ 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,
+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
@@ -272,7 +273,7 @@ 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
+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
@@ -280,7 +281,7 @@ 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
+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
-- 
cgit v1.2.3


From bbfa17765599a04931efa68a5397f418e6ea5b39 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 6 Nov 2015 09:18:54 +0100
Subject: Prehistory of Coq: consistency.

Don't use abbreviated first names in sentences.
---
 dev/doc/README-V1-V5.asciidoc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc
index 43971ba553..a02f0831dc 100644
--- a/dev/doc/README-V1-V5.asciidoc
+++ b/dev/doc/README-V1-V5.asciidoc
@@ -194,7 +194,7 @@ 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
+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.
 
@@ -227,7 +227,7 @@ 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. Huet.
+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,
-- 
cgit v1.2.3


From 856e746e2a0adf959faee0907555af81be11d027 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 6 Nov 2015 09:26:50 +0100
Subject: Prehistory of Coq: justification of the plain text.

---
 dev/doc/README-V1-V5.asciidoc | 483 ++++++++++++++++++++++--------------------
 1 file changed, 254 insertions(+), 229 deletions(-)

(limited to 'dev')

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 +
-- 
cgit v1.2.3


From fd7eb1dd0f2cf5fab3a6a2a5f567acaca2defed5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 11 Nov 2015 00:02:21 +0100
Subject: Prehistory of Coq: move the bibliographic references to a dedicated
 section.

So as not to clutter the text. Also took the opportunity to add a few missing references.
---
 dev/doc/README-V1-V5.asciidoc | 121 +++++++++++++++++++++++++++---------------
 1 file changed, 79 insertions(+), 42 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc
index 4395fd0e5c..9a4261b3a7 100644
--- a/dev/doc/README-V1-V5.asciidoc
+++ b/dev/doc/README-V1-V5.asciidoc
@@ -45,10 +45,8 @@ 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.
+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
@@ -63,19 +61,14 @@ 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.
+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
+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.
+Constructions__<<CH87>>.
 
 Version 2.8 was frozen on December 16th, 1985, and served for
 developing the exemples in the above papers.
@@ -86,12 +79,9 @@ 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__ <<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.
@@ -102,9 +92,8 @@ 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 __Induction Principles Formalized in the Calculus of
+Constructions__ <<H88>>.
 
 Version 3
 ---------
@@ -263,14 +252,12 @@ 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 <<C90>>,
 - _Inductive definitions in the Calculus of Constructions_, by
-   Christine Paulin-Mohring,
+   Christine Paulin-Mohrin,
 - _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
+  Constructions_, by Christine Paulin-Mohring <<P89>>,
+- _The Constructive Engine_, by Gérard Huet <<H89>>,
 
 as well as a number of user guides:
 
@@ -286,22 +273,15 @@ 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__ <<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_. 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__ <<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
@@ -335,4 +315,61 @@ section of Coq's Reference Manual.
 ====
 September 2015 +
 Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.
-====
\ No newline at end of file
+====
+
+[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.
-- 
cgit v1.2.3


From 7978e1dbd6dcd409b0b98a4b407a66b104dff3ba Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 12 Nov 2015 11:59:33 +0100
Subject: Script building MacOS package.

---
 dev/make-macos-dmg.sh | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100755 dev/make-macos-dmg.sh

(limited to 'dev')

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
new file mode 100755
index 0000000000..8f6a7f9e1b
--- /dev/null
+++ b/dev/make-macos-dmg.sh
@@ -0,0 +1,31 @@
+#!/bin/bash
+
+# Fail on first error
+set -e
+
+# Configuration setup
+eval `opam config env`
+make distclean
+OUTDIR=$PWD/_install
+DMGDIR=$PWD/_dmg
+./configure -debug -prefix $OUTDIR
+VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
+APP=bin/CoqIDE_${VERSION}.app
+
+# Create a .app file with CoqIDE
+~/.local/bin/jhbuild run make -j -l2 $APP
+
+# Build Coq and run test-suite
+make && make check
+
+# Add Coq to the .app file
+make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
+
+# Sign the .app file
+codesign -f -s - $APP
+
+# Create the dmg bundle
+mkdir $DMGDIR
+ln -s /Applications $DMGDIR
+cp -r $APP $DMGDIR
+hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
-- 
cgit v1.2.3


From 2fd497d380de998c4b22b9f7167eb4023e4cd576 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 13 Nov 2015 14:21:01 +0100
Subject: MacOS package script: do not fail if directory _dmg already exists.

---
 dev/make-macos-dmg.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index 8f6a7f9e1b..a8b5d10dad 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -25,7 +25,7 @@ make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq insta
 codesign -f -s - $APP
 
 # Create the dmg bundle
-mkdir $DMGDIR
+mkdir -p $DMGDIR
 ln -s /Applications $DMGDIR
 cp -r $APP $DMGDIR
 hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
-- 
cgit v1.2.3


From 8e482fc932fa2b1893025d914d42dd17881c2fac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2015 18:51:33 +0100
Subject: Being more precise and faithful about the origin of the file
 reporting about the prehistory of Coq.

---
 dev/doc/README-V1-V5 | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5
index 2ca62e3d74..ebbc057734 100644
--- a/dev/doc/README-V1-V5
+++ b/dev/doc/README-V1-V5
@@ -1,10 +1,13 @@
 
                  Notes on the prehistory of Coq
 
-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 Ecole Normale Supérieure
-of Paris, from 1984 onwards.
+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
 
-- 
cgit v1.2.3


From 23e6963a8168756f225ea2ae75fcf2af6952c6c3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 18 Nov 2015 14:50:35 +0100
Subject: MacOS package script: do not fail if link to /Applications already
 exists.

---
 dev/make-macos-dmg.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index a8b5d10dad..70889badc1 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -26,6 +26,6 @@ codesign -f -s - $APP
 
 # Create the dmg bundle
 mkdir -p $DMGDIR
-ln -s /Applications $DMGDIR
+ln -sf /Applications $DMGDIR/Applications
 cp -r $APP $DMGDIR
 hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
-- 
cgit v1.2.3


From 7a33a6284ba4e0953f82cf436fe324cdb95497e7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2015 12:10:29 +0100
Subject: Update history of revisions.

---
 dev/doc/versions-history.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 1b1d3500a4..492e75a7bb 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -223,6 +223,7 @@ version & date & comments \\
 Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\
  & & to Caml Special Light (to later become Objective Caml)\\
  & & has implicit arguments and coercions\\
+ & & has coinductive types\\
 
 Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\
  & & \feature{omega} [10-9-1996] \\
-- 
cgit v1.2.3


From d1c4ea65c490b59d34a5464554237a270063cbc9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 19 Nov 2015 22:32:54 +0100
Subject: Ensuring that documentation of mli code works in the presence of
 utf-8 characters.

---
 dev/ocamldoc/fix-ocamldoc-utf8 |  6 ++++++
 dev/ocamldoc/header.tex        | 14 ++++++++++++++
 2 files changed, 20 insertions(+)
 create mode 100755 dev/ocamldoc/fix-ocamldoc-utf8
 create mode 100644 dev/ocamldoc/header.tex

(limited to 'dev')

diff --git a/dev/ocamldoc/fix-ocamldoc-utf8 b/dev/ocamldoc/fix-ocamldoc-utf8
new file mode 100755
index 0000000000..fe2e0c1155
--- /dev/null
+++ b/dev/ocamldoc/fix-ocamldoc-utf8
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+# This reverts automatic translation of latin1 accentuated letters by ocamldoc
+# Usage: fix-ocamldoc-utf8 file
+
+sed -i -e 's/\\`a/\d224/g' -e "s/\\\^a/\d226/g" -e "s/\\\'e/\d233/g" -e 's/\\`e/\d232/g' -e "s/\\\^e/\d234/g" -e 's/\\\"e/\d235/g' -e "s/\\\^o/\d244/g" -e 's/\\\"o/\d246/g' -e "s/\\\^i/\d238/g" -e 's/\\\"i/\d239/g' -e 's/\\`u/\d249/g' -e "s/\\\^u/\d251/g" -e "s/\\\c{c}/\d231/g" $1
diff --git a/dev/ocamldoc/header.tex b/dev/ocamldoc/header.tex
new file mode 100644
index 0000000000..4091f8144f
--- /dev/null
+++ b/dev/ocamldoc/header.tex
@@ -0,0 +1,14 @@
+\documentclass[11pt]{article} 
+\usepackage[utf8x]{inputenc} 
+\usepackage[T1]{fontenc} 
+\usepackage{textcomp}
+\usepackage{tipa}
+\usepackage{textgreek}
+\usepackage{fullpage} 
+\usepackage{url} 
+\usepackage{ocamldoc}
+\title{Coq mlis documentation}
+\begin{document}
+\maketitle
+\tableofcontents
+\vspace{0.2cm}
-- 
cgit v1.2.3


From 126a3c998c62bfd9f9b570f12b2e29576dd94cdd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 5 Dec 2015 13:43:07 +0100
Subject: Factorizing unsafe code by relying on the new Dyn module.

---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 1a2819feb2..b498c2659d 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -8,6 +8,7 @@ Hashcons
 CSet
 CMap
 Int
+Dyn
 HMap
 Option
 Store
@@ -36,7 +37,6 @@ Util
 Ppstyle
 Errors
 Bigint
-Dyn
 CUnix
 System
 Envars
-- 
cgit v1.2.3


From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 dev/v8-syntax/syntax-v8.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 6630be06ab..64431ea161 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -81,7 +81,7 @@ Parenthesis are used to group regexps. Beware to distinguish this operator
 $\GR{~}$ from the terminals $\ETERM{( )}$, and $\mid$ from terminal
 \TERMbar.
 
-Rules are optionaly annotated in the right margin with:
+Rules are optionally annotated in the right margin with:
 \begin{itemize}
 \item a precedence and associativity (L for left, R for right and N for no associativity), indicating how to solve conflicts;
   lower levels are tighter;
-- 
cgit v1.2.3


From 19ea51a4b7f7debbe5bdeb2b2689cddadd9876f4 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 7 Dec 2015 16:25:58 +0100
Subject: Fixing a minor problem in Makefile.build that was prevening
 "dev/printers.cma" to be loadable within "ocamldebug".

---
 dev/db | 2 --
 1 file changed, 2 deletions(-)

(limited to 'dev')

diff --git a/dev/db b/dev/db
index f259b50eb3..36a171af1c 100644
--- a/dev/db
+++ b/dev/db
@@ -1,5 +1,3 @@
-load_printer "gramlib.cma"
-load_printer "str.cma"
 load_printer "printers.cma"
 
 install_printer Top_printers.ppfuture
-- 
cgit v1.2.3


From eee16239f6b00400c8a13b787c310bcb11c37afe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Dec 2015 12:06:24 +0100
Subject: Tying the loop in tactic printing API.

---
 dev/top_printers.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b3b1ae0e91..0e90026122 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -468,9 +468,8 @@ let pp_generic_argument arg =
 
 let prgenarginfo arg =
   let tpe = pr_argument_type (genarg_tag arg) in
-  let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in
   try
-    let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in
+    let data = Pptactic.pr_top_generic (Global.env ()) arg in
     str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
   with _any ->
     str "<genarg:" ++ tpe ++ str ">"
-- 
cgit v1.2.3


From b2beb9087628de23679a831e6273b91816f1ed27 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 17 Dec 2015 19:24:17 +0100
Subject: Using dynamic values in tactic evaluation.

---
 dev/top_printers.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0e90026122..20c8f690bd 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -467,11 +467,13 @@ let pp_generic_argument arg =
   pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
 
 let prgenarginfo arg =
-  let tpe = pr_argument_type (genarg_tag arg) in
-  try
-    let data = Pptactic.pr_top_generic (Global.env ()) arg in
-    str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
-  with _any ->
+  let Val.Dyn (tag, _) = arg in
+  let tpe = str (Val.repr tag) in
+  (** FIXME *)
+(*   try *)
+(*     let data = Pptactic.pr_top_generic (Global.env ()) arg in *)
+(*     str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *)
+(*   with _any -> *)
     str "<genarg:" ++ tpe ++ str ">"
 
 let ppgenarginfo arg = pp (prgenarginfo arg)
-- 
cgit v1.2.3


From 44ac395761d6b46866823b89addaea0ab45f4ebc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Dec 2015 00:38:00 +0100
Subject: Finer-grained types for toplevel values.

---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 20c8f690bd..0894e0378d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -468,7 +468,7 @@ let pp_generic_argument arg =
 
 let prgenarginfo arg =
   let Val.Dyn (tag, _) = arg in
-  let tpe = str (Val.repr tag) in
+  let tpe = Val.repr tag in
   (** FIXME *)
 (*   try *)
 (*     let data = Pptactic.pr_top_generic (Global.env ()) arg in *)
-- 
cgit v1.2.3


From a5e1b40b93e47a278746ee6752474891cd856c29 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 31 Dec 2015 19:26:02 +0100
Subject: Simplification of grammar_prod_item type.

Actually the identifier was never used and just carried along.
---
 dev/top_printers.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0894e0378d..cbebcdfcd4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,8 +520,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")),
-	 Some (Names.Id.of_string "c"))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
 
 let _ =
   try
@@ -537,8 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")),
-	 Some (Names.Id.of_string "c"))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
 
 (* Setting printer of unbound global reference *)
 open Names
-- 
cgit v1.2.3


From 8a9445fbf65d4ddf2c96348025d487b4d54a5d01 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 5 Jan 2016 19:36:02 +0100
Subject: Fix order of files in mllib.

CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
---
 dev/printers.mllib | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 07b48ed573..eeca6809ae 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -16,6 +16,8 @@ Backtrace
 IStream
 Pp_control
 Loc
+CList
+CString
 Compat
 Flags
 Control
@@ -28,8 +30,6 @@ Segmenttree
 Unicodetable
 Unicode
 CObj
-CList
-CString
 CArray
 CStack
 Util
-- 
cgit v1.2.3


From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 8 Jan 2016 10:00:21 +0100
Subject: CLEANUP: kernel/context.ml{,i}

The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.

Some missing comments were added to the *.mli file.

The output of ocamldoc was checked whether it looks in a reasonable way.

"TODO: cleanup" was removed

The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)

The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)

The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)

The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})

The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.

Thrown exceptions are now documented.

Naming of formal parameters was made more consistent across different functions.

Comments of similar functions in different modules are now consistent.

Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
 It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
 we can see the comments also there and do not need to open a different file if we want to see it.)

When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)

"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)

An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
---
 dev/doc/changes.txt | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2f62be9aff..c143afd374 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,3 +1,53 @@
+=========================================
+= CHANGES BETWEEN COQ V8.5 AND CQQ V8.6 =
+=========================================
+
+- 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
+    Context.map_named_list_declaration   --->  Context.NamedList.Declaration.map
+    Context.map_rel_declaration          --->  Context.Rel.Declaration.map
+    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
+    Context.map_named_context            --->  Context.Named.map
+    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
+
 =========================================
 = CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 =
 =========================================
-- 
cgit v1.2.3


From 2d568a895d5c8a246f497c94c79811d3aad4269f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Jan 2016 00:20:46 +0100
Subject: Fixing #4467 (continued).

Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
---
 dev/printers.mllib | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index eeca6809ae..ab7e9fc346 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -160,14 +160,14 @@ Constrarg
 Constrexpr_ops
 Genintern
 Notation_ops
-Topconstr
 Notation
 Dumpglob
+Syntax_def
+Smartlocate
+Topconstr
 Reserve
 Impargs
-Syntax_def
 Implicit_quantifiers
-Smartlocate
 Constrintern
 Modintern
 Constrextern
-- 
cgit v1.2.3


From 448866f0ec5291d58677d8fccbefde493ade0ee2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Jan 2016 22:20:16 +0100
Subject: Removing constr generic argument.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index cbebcdfcd4..cc1cf23d60 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -510,7 +510,7 @@ let _ =
   try
     Vernacinterp.vinterp_add false ("PrintConstr", 0)
       (function
-         [c] when genarg_tag c = ConstrArgType && true ->
+         [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
@@ -526,7 +526,7 @@ let _ =
   try
     Vernacinterp.vinterp_add false ("PrintPureConstr", 0)
       (function
-         [c] when genarg_tag c = ConstrArgType && true ->
+         [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
-- 
cgit v1.2.3


From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

---
 dev/db_printers.ml  | 2 +-
 dev/header          | 2 +-
 dev/top_printers.ml | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/db_printers.ml b/dev/db_printers.ml
index e843bbc518..500595085e 100644
--- a/dev/db_printers.ml
+++ b/dev/db_printers.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/dev/header b/dev/header
index e5184df31c..4132051791 100644
--- a/dev/header
+++ b/dev/header
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9f2e1b09e..6e5b048ccd 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3


From aa1913411547eeed464b024f1cf54113be26e929 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 21 Jan 2016 22:17:36 +0100
Subject: Compile OS X binaries without native_compute support.

---
 dev/make-macos-dmg.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index 70889badc1..20b7b5b531 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -8,7 +8,7 @@ eval `opam config env`
 make distclean
 OUTDIR=$PWD/_install
 DMGDIR=$PWD/_dmg
-./configure -debug -prefix $OUTDIR
+./configure -debug -prefix $OUTDIR -native-compiler no
 VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
 APP=bin/CoqIDE_${VERSION}.app
 
-- 
cgit v1.2.3


From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 29 Jan 2016 10:13:12 +0100
Subject: CLEANUP: Context.{Rel,Named}.Declaration.t

  Originally, rel-context was represented as:

    Context.rel_context = Names.Name.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Rel.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.t = LocalAssum of Names.Id.t * Constr.t
                    | LocalDef of Names.Id.t * Constr.t * Constr.t

Motivation:

  (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
      function which looked like this:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      Suppose that you do not know about rel-context and named-context.
      (that is the case of people who just started to read the source code)
      Merlin would tell you that the type of the value you are destructing
      by "match" is:

        'a * 'b option * Constr.t                    (* worst-case scenario *)

      or

        Named.Name.t * Constr.t option * Constr.t    (* best-case scenario (?) *)

      To me, this is akin to wearing an opaque veil.
      It is hard to figure out the meaning of the values you are looking at.
      In particular, it is hard to discover the connection between the value
      we are destructing above and the datatypes and functions defined
      in the "kernel/context.ml" file.

      In this case, the connection is there, but it is not visible
      (between the function above and the "Context" module).

      ------------------------------------------------------------------------

      Now consider, what happens when the reader see the same function
      presented in the following form:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
      to jump to the corresponding definition and learn more.

      In this case, the connection is there, and it is directly visible
      (between the function above and the "Context" module).

  (2) Also, if we already have the concepts such as:
      - local declaration
      - local assumption
      - local definition
      and we describe these notions meticulously in the Reference Manual,
      then it is a real pity not to reinforce the connection
      of the actual code with the abstract description we published.
---
 dev/doc/changes.txt | 31 +++++++++++++++++++++++++------
 1 file changed, 25 insertions(+), 6 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index c143afd374..0581a5f850 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,5 +1,5 @@
 =========================================
-= CHANGES BETWEEN COQ V8.5 AND CQQ V8.6 =
+= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
 - The interface of the Context module was changed.
@@ -9,9 +9,9 @@
     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
+    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
+    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
@@ -37,8 +37,8 @@
     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
-    Context.map_named_context            --->  Context.Named.map
+    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
@@ -48,8 +48,27 @@
     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.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.t = LocalAssum of Names.Id.t * Constr.t
+	            | LocalDef of Names.Id.t * Constr.t * Constr.t
+
+
 =========================================
-= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 =
+= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
 =========================================
 
 ** Refactoring : more mli interfaces and simpler grammar.cma **
-- 
cgit v1.2.3


From 78b5670a0a1cf7ba31acabe710b311bf13df8745 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 3 Mar 2016 20:34:35 -0500
Subject: Fix a typo in dev/doc/changes.txt

CQQ -> COQ---
 dev/doc/changes.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2f62be9aff..f7621a4076 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,5 +1,5 @@
 =========================================
-= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 =
+= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
 =========================================
 
 ** Refactoring : more mli interfaces and simpler grammar.cma **
-- 
cgit v1.2.3


From b98e4857a13a4014c65882af5321ebdb09f41890 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 4 Mar 2016 17:40:10 +0100
Subject: Rename Ephemeron -> CEphemeron.

Fixes compilation of Coq with OCaml 4.03 beta 1.
---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index ab7e9fc346..ad9a5d75e6 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -48,7 +48,7 @@ Rtree
 Heap
 Genarg
 Stateid
-Ephemeron
+CEphemeron
 Future
 RemoteCounter
 Monad
-- 
cgit v1.2.3


From d3653c6da5770dfc4d439639b49193e30172763a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Mar 2016 15:10:27 +0100
Subject: Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND
 move.

We just reuse the same one weird old trick in CAMLP4 to compare keywords and
identifiers as tokens. Note though that the commit 982460743 does not fix the
keyword vs. identifier issue in CAMLP4, so that the corresponding test fails.
This means that since that commit, some code compiling with CAMLP5 does not
when using CAMLP4, making it a second-class citizen.
---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 21868203f8..39e4b1cdb1 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -19,6 +19,7 @@ Pp_control
 Loc
 CList
 CString
+Tok
 Compat
 Flags
 Control
@@ -153,7 +154,6 @@ Library
 States
 
 Genprint
-Tok
 Lexer
 Ppextend
 Pputils
-- 
cgit v1.2.3


From 6ecbc9990a49a0dd51970c7fc8b13f39f02be773 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Mar 2016 18:34:39 +0100
Subject: Moving Ltac traces to Tacexpr and Tacinterp.

---
 dev/printers.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 39e4b1cdb1..34bde1ac27 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -174,7 +174,6 @@ Implicit_quantifiers
 Constrintern
 Modintern
 Constrextern
-Proof_type
 Goal
 Miscprint
 Logic
-- 
cgit v1.2.3


From 9e96794d6a4327761ce1ff992351199919431be1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Mar 2016 19:01:38 +0100
Subject: Moving Tactic_debug to tactics/ folder.

---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 34bde1ac27..d8fb2b906c 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -187,13 +187,13 @@ Proofview
 Proof
 Proof_global
 Pfedit
-Tactic_debug
 Decl_mode
 Ppconstr
 Entry
 Pcoq
 Printer
 Pptactic
+Tactic_debug
 Ppdecl_proof
 Egramml
 Egramcoq
-- 
cgit v1.2.3


From cdc91f02f98b4d857bfebe61d95b920787a8d0e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Mar 2016 21:25:20 +0100
Subject: Putting Tactic_debug just below Tacinterp.

---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index d8fb2b906c..7710033dba 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -193,12 +193,12 @@ Entry
 Pcoq
 Printer
 Pptactic
-Tactic_debug
 Ppdecl_proof
 Egramml
 Egramcoq
 Tacsubst
 Tacenv
+Tactic_debug
 Trie
 Dn
 Btermdn
-- 
cgit v1.2.3


From a6d048a2de62bba97948fee2937dc5ea2fad0c83 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Mar 2016 07:33:19 +0100
Subject: Removing an empty file detected by Luc Grateau.

---
 dev/tools/Makefile.common | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 delete mode 100644 dev/tools/Makefile.common

(limited to 'dev')

diff --git a/dev/tools/Makefile.common b/dev/tools/Makefile.common
deleted file mode 100644
index e69de29bb2..0000000000
-- 
cgit v1.2.3


From e171456870f9893d582d53114d4f87e634c007e5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Mar 2016 14:24:33 +0100
Subject: Trying to circumvent hdiutil error 5341 by padding.

When generating the OS X Coq + CoqIDE bundle, hdiutil often produces error
5341. This seems to be a known bug on Apple's side, occurring for some sizes of
dmg files. We try to change the current (problematic) size by adding a file
full of random bits.
---
 dev/make-macos-dmg.sh | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev')

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index 20b7b5b531..b43ada9076 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -28,4 +28,8 @@ codesign -f -s - $APP
 mkdir -p $DMGDIR
 ln -sf /Applications $DMGDIR/Applications
 cp -r $APP $DMGDIR
+
+# Temporary countermeasure to hdiutil error 5341
+head -c9703424 /dev/urandom > $DMGDIR/.padding
+
 hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
-- 
cgit v1.2.3


From f8f1f9d38bf2d35b0dc69fbf2e8ebbfc04b1a82d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Mar 2016 01:36:39 +0100
Subject: Documenting the change of EXTEND macros.

---
 dev/doc/changes.txt | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 0581a5f850..1f5ba7862f 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -66,6 +66,15 @@
     Context.Named.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.
 
 =========================================
 = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
-- 
cgit v1.2.3


From a99aa093b962e228817066d00f7e12698f8df73a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Mar 2016 22:27:17 +0100
Subject: Simplifying the code of Entry.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index aef9b10b26..b8bc0483d3 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,7 +520,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 let _ =
   try
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
-- 
cgit v1.2.3


From 805c8987fbb5fdeb94838bb5a3a7364c0a3d3374 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 17 Feb 2016 13:45:24 +0100
Subject: Do not export entry_key from Pcoq anymore.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b8bc0483d3..141eab3f3f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,7 +520,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
+        (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 let _ =
   try
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
+        (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
-- 
cgit v1.2.3


From 93a77f3cb8ee36072f93b4c0ace6f0f9c19f51a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 18:41:37 +0100
Subject: Moving Refine to its proper module.

---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 7710033dba..c46f6b72a4 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -184,6 +184,7 @@ Proof_errors
 Logic_monad
 Proofview_monad
 Proofview
+Refine
 Proof
 Proof_global
 Pfedit
-- 
cgit v1.2.3


From 08c31f46aa05098e1a97d9144599c1e5072b7fc3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 19:52:54 +0100
Subject: Pushing Proofview further down the dependency alley.

---
 dev/printers.mllib | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index c46f6b72a4..db86bb5edd 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -141,6 +141,9 @@ Find_subterm
 Tacred
 Classops
 Typeclasses_errors
+Logic_monad
+Proofview_monad
+Proofview
 Typeclasses
 Detyping
 Indrec
@@ -181,9 +184,6 @@ Refiner
 Clenv
 Evar_refiner
 Proof_errors
-Logic_monad
-Proofview_monad
-Proofview
 Refine
 Proof
 Proof_global
-- 
cgit v1.2.3


From e98d7276f52c4b67bf05a80a6b44f334966f82fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 20:11:50 +0100
Subject: Splitting Evarutil in two distinct files.

Some parts of Evarutils were related to the management of evars under constraints.
We put them in the Evardefine file.
---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index db86bb5edd..4830b36ab5 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -131,6 +131,7 @@ Retyping
 Cbv
 Pretype_errors
 Evarutil
+Evardefine
 Evarsolve
 Recordops
 Evarconv
-- 
cgit v1.2.3


From c3de822e711fa3f10817432b7023fc2f88c0aeeb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 20:41:17 +0100
Subject: Making Evarutil independent from Reductionops.

---
 dev/printers.mllib | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 4830b36ab5..a3ba42ba78 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -123,14 +123,15 @@ Evd
 Sigma
 Glob_ops
 Redops
+Pretype_errors
+Evarutil
 Reductionops
 Inductiveops
 Arguments_renaming
 Nativenorm
 Retyping
 Cbv
-Pretype_errors
-Evarutil
+
 Evardefine
 Evarsolve
 Recordops
-- 
cgit v1.2.3


From 6d87fd89abdf17ddd4864386d66bb06f0d0a151f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 21:20:29 +0100
Subject: Documenting changes.

---
 dev/doc/changes.txt | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 1f5ba7862f..2f631c6338 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -76,6 +76,11 @@
   the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
   in the parsing rules, so beware of recursive calls.
 
+- 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.
+
 =========================================
 = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
 =========================================
-- 
cgit v1.2.3


From f39543a752d05e5661749bbc3f221d75e525b3b4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 03:10:54 +0100
Subject: Moving Tactic_debug to Hightactic.

---
 dev/printers.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index a3ba42ba78..aad56f586b 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -201,7 +201,6 @@ Egramml
 Egramcoq
 Tacsubst
 Tacenv
-Tactic_debug
 Trie
 Dn
 Btermdn
-- 
cgit v1.2.3


From 6de9f13ba666250ea397c7db1d9d37075a9dc1c2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 03:37:55 +0100
Subject: Moving Tacenv to Hightactics.

---
 dev/printers.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index aad56f586b..9f25ba55e7 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -200,7 +200,6 @@ Ppdecl_proof
 Egramml
 Egramcoq
 Tacsubst
-Tacenv
 Trie
 Dn
 Btermdn
-- 
cgit v1.2.3


From a581331f26d96d1a037128ae83bebd5e6c27f665 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Mar 2016 00:26:02 +0100
Subject: Creating a dedicated ltac/ folder for Hightactics.

---
 dev/base_include                | 1 +
 dev/doc/coq-src-description.txt | 7 -------
 dev/ocamldebug-coq.run          | 2 +-
 3 files changed, 2 insertions(+), 8 deletions(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index 767e023ea2..86f34b2ac9 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -17,6 +17,7 @@
 #directory "grammar";;
 #directory "intf";;
 #directory "stm";;
+#directory "ltac";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index fe896d3160..00e7f5c53c 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/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index b00d084edb..f9310e076a 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -20,7 +20,7 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/library -I $COQTOP/engine \
 	-I $COQTOP/pretyping -I $COQTOP/parsing \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
-	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
+	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
         -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
         -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
-- 
cgit v1.2.3


From f9ef1441083a988a938e163393dfbab04ab9da18 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 7 Apr 2016 13:52:03 +0200
Subject: Use -win32 and -win64 suffixes for installer name on Windows.

---
 dev/make-installer-win32.sh | 2 +-
 dev/make-installer-win64.sh | 2 +-
 dev/nsis/coq.nsi            | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh
index d405e66cc0..51d428dd1e 100755
--- a/dev/make-installer-win32.sh
+++ b/dev/make-installer-win32.sh
@@ -16,7 +16,7 @@ if [ ! -e bin/make.exe ]; then
 fi
 VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
 cd dev/nsis
-"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win32" coq.nsi
 echo Installer:
 ls -h $PWD/*exe
 cd ../..
diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh
index 2f765c1a10..438f4ae5b7 100755
--- a/dev/make-installer-win64.sh
+++ b/dev/make-installer-win64.sh
@@ -22,7 +22,7 @@ if [ ! -e bin/make.exe ]; then
 fi
 VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
 cd dev/nsis
-"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win64" coq.nsi
 echo Installer:
 ls -h $PWD/*exe
 cd ../..
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index 676490510c..e1052b1e1b 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -13,7 +13,7 @@ SetCompressor lzma
 
 !define MY_PRODUCT "Coq" ;Define your own software name here
 !define COQ_SRC_PATH "..\.."
-!define OUTFILE "coq-installer-${VERSION}.exe"
+!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe"
 
 !include "MUI2.nsh"
 !include "FileAssociation.nsh"
-- 
cgit v1.2.3


From b5420538da04984ca42eb4284a9be27f3b5ba021 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 8 Apr 2016 00:58:56 +0200
Subject: Fixing printing of toplevel values.

This is not perfect yet, in particular the whole precedence system is a real
mess, as there is a real need for tidying up the Pptactic implementation.
Nonetheless, printing toplevel values is only used for debugging purposes, where
an ugly display is better than none at all.
---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 141eab3f3f..29ea08e025 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -468,7 +468,7 @@ let pp_generic_argument arg =
 
 let prgenarginfo arg =
   let Val.Dyn (tag, _) = arg in
-  let tpe = Val.repr tag in
+  let tpe = Val.pr tag in
   (** FIXME *)
 (*   try *)
 (*     let data = Pptactic.pr_top_generic (Global.env ()) arg in *)
-- 
cgit v1.2.3