13 files changed, 72 insertions, 385 deletions
diff --git a/dev/README.md b/dev/README.md
index d9fdd230d3..9761f7b96f 100644
--- a/dev/README.md
+++ b/dev/README.md
@@ -25,7 +25,6 @@
 | [`dev/doc/universes.txt`](doc/universes.txt) |  Help for debugging universes |
 | [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND |
 | [`dev/doc/perf-analysis`](doc/perf-analysis)|  Analysis of perfs measured on the compilation of user contribs |
-| [`dev/doc/cic.dtd`](doc/cic.dtd) | Official dtd of the calc. of ind. constr. for im/ex-portation |
 | [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine |
 | [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections |
 | [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine |
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 8489bcfc3a..c8cfcf60c8 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -373,7 +373,8 @@ IF "%RUNSETUP%"=="Y" (
     -P make,unzip ^
     -P gdb,liblzma5 ^
     -P patch,automake1.14 ^
-    -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
+    -P pkg-config ^
+    -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-windows_default_manifest ^
     -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
     -P libiconv-devel,libunistring-devel,libncurses-devel ^
     -P gettext-devel,libgettextpo-devel ^
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 2e934ff0c0..43f44a80b4 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1202,7 +1202,7 @@ function make_lablgtk {
   make_gtk_sourceview2
   if build_prep https://forge.ocamlcore.org/frs/download.php/1726 lablgtk-2.18.6 tar.gz 1 ; then
     # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
-    cp "/bin/$TARGET_ARCH-pkg-config.exe"  bin_special/pkg-config.exe
+    cp "/bin/$TARGET_ARCH-pkg-config"  bin_special/pkg-config
     logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML"
 
     # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 74e8d3bbaa..deeec3942d 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -289,3 +289,10 @@
 : "${verdi_raft_CI_REF:=master}"
 : "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}"
 : "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}"
+
+########################################################################
+# stdlib2
+########################################################################
+: "${stdlib2_CI_REF:=master}"
+: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}"
+: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-stdlib2.sh b/dev/ci/ci-stdlib2.sh
new file mode 100755
index 0000000000..ec1c180d7d
--- /dev/null
+++ b/dev/ci/ci-stdlib2.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download stdlib2
+
+( cd "${CI_BUILD_DIR}/stdlib2/src" && ./bootstrap && make && make install)
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 43278c37b1..ac763547b6 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-02-17-V1"
+# CACHEKEY: "bionic_coq-V2019-03-11-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.3.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
     CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh
new file mode 100644
index 0000000000..2b4c1489ad
--- /dev/null
+++ b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh
@@ -0,0 +1,13 @@
+_OVERLAY_BRANCH=ho-matching-occ-sel
+
+if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    unicoq_CI_REF="PR7819-overlay"
+
+    mtac2_CI_REF="PR7819-overlay"
+    mtac2_CI_GITURL=https://github.com/mattam82/Mtac2
+
+    equations_CI_GITURL=https://github.com/mattam82/Coq-Equations
+    equations_CI_REF="PR7819-overlay"
+
+fi
diff --git a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh
new file mode 100644
index 0000000000..1110157069
--- /dev/null
+++ b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9389" ] || [ "$CI_BRANCH" = "set-implicits" ]; then
+
+    equations_CI_REF=set-implicits
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    mtac2_CI_REF=set-implicits
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
new file mode 100644
index 0000000000..1af8b5430d
--- /dev/null
+++ b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then
+
+    quickchick_CI_REF=context-constructor
+    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+    equations_CI_REF=context-constructor
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc
deleted file mode 100644
index 631fb92c97..0000000000
--- a/dev/doc/README-V1-V5.asciidoc
+++ /dev/null
@@ -1,378 +0,0 @@
-Notes on the prehistory of Coq
-==============================
-:author:  Thierry Coquand, Gérard Huet & Christine Paulin-Mohring
-:revdate: September 2015
-:toc:
-:toc-placement: preamble
-:toclevels: 1
-:showtitle:
-
-
-This document is a copy within the Coq archive of a document written
-in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin
-to accompany their public release of the archive of versions 1.10 to 6.2
-of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and
-implemented in the Formel team, joint between the INRIA Rocquencourt
-laboratory and the Ecole Normale Supérieure of Paris, from 1984
-onwards.
-
-Version 1
----------
-
-This software is a prototype type-checker for a higher-order logical
-formalism known as the Theory of Constructions, presented in his PhD
-thesis by Thierry Coquand, with influences from Girard's system F and
-de Bruijn's Automath.  The metamathematical analysis of the system is
-the PhD work of Thierry Coquand. The software is mostly the work of
-Gérard Huet.  Most of the mathematical examples verified with the
-software are due to Thierry Coquand.
-
-The programming language of the CONSTR software (as it was called at
-the time) was a version of ML adapted from the Edinburgh LCF system
-and running on a LISP backend. The main improvements from the original
-LCF ML were that ML was compiled rather than interpreted (Gérard Huet
-building on the original translator by Lockwood Morris), and that it
-was enriched by recursively defined types (work of Guy
-Cousineau). This ancestor of CAML was used and improved by Larry
-Paulson for his implementation of Cambridge LCF.
-
-Software developments of this prototype occurred from late 1983 to
-early 1985.
-
-Version 1.10 was frozen on December 22nd 1984. It is the version used
-for the examples in Thierry Coquand's thesis, defended on January 31st
-1985.  There was a unique binding operator, used both for universal
-quantification (dependent product) at the level of types and
-functional abstraction (λ) at the level of terms/proofs, in the manner
-of Automath. Substitution (λ-reduction) was implemented using de
-Bruijn's indexes.
-
-Version 1.11 was frozen on February 19th, 1985. It is the version used
-for the examples in the paper: Th. Coquand, G. Huet. __Constructions: A
-Higher Order Proof System for Mechanizing Mathematics__ <<CH85>>.
-
-Christine Paulin joined the team at this point, for her DEA research
-internship.  In her DEA memoir (August 1985) she presents developments
-for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such
-that _f(m)_ is greater than _n_, for _f_ an increasing integer
-function, a challenge for constructive mathematics. She also encoded
-the majority voting algorithm of Boyer and Moore.
-
-Version 2
----------
-
-The formal system, now renamed as the _Calculus of Constructions_, was
-presented with a proof of consistency and comparisons with proof
-systems of Per Martin Löf, Girard, and the Automath family of N. de
-Bruijn, in the paper: T. Coquand and G. Huet. __The Calculus of
-Constructions__ <<CH88>>.
-
-An abstraction of the software design, in the form of an abstract
-machine for proof checking, and a fuller sequence of mathematical
-developments was presented in: Th. Coquand, G. Huet. __Concepts
-Mathématiques et Informatiques Formalisés dans le Calcul des
-Constructions__<<CH87>>.
-
-Version 2.8 was frozen on December 16th, 1985, and served for
-developing the exemples in the above papers.
-
-This calculus was then enriched in version 2.9 with a cumulative
-hierarchy of universes. Universe levels were initially explicit
-natural numbers.  Another improvement was the possibility of automatic
-synthesis of implicit type arguments, relieving the user of tedious
-redundant declarations.
-
-Christine Paulin wrote an article __Algorithm development in the
-Calculus of Constructions__ <<P86>>. Besides _lambo_ and _majority_,
-she presents quicksort and a text formatting algorithm.
-
-Version 2.13 of the Calculus of Constructions with universes was
-frozen on June 25th, 1986.
-
-A synthetic presentation of type theory along constructive lines with
-ML algorithms was given by Gérard Huet in his May 1986 CMU course
-notes _Formal Structures for Computation and Deduction_. Its chapter
-_Induction and Recursion in the Theory of Constructions_ was presented
-as an invited paper at the Joint Conference on Theory and Practice of
-Software Development TAPSOFT’87 at Pise in March 1987, and published
-as __Induction Principles Formalized in the Calculus of
-Constructions__ <<H88>>.
-
-Version 3
----------
-
-This version saw the beginning of proof automation, with a search
-algorithm inspired from PROLOG and the applicative logic programming
-programs of the course notes _Formal structures for computation and
-deduction_.  The search algorithm was implemented in ML by Thierry
-Coquand.  The proof system could thus be used in two modes: proof
-verification and proof synthesis, with tactics such as `AUTO`.
-
-The implementation language was now called CAML, for Categorical
-Abstract Machine Language. It used as backend the LLM3 virtual machine
-of Le Lisp by Jérôme Chailloux. The main developers of CAML were
-Michel Mauny, Ascander Suarez and Pierre Weis.
-
-V3.1 was started in the summer of 1986, V3.2 was frozen at the end of
-November 1986. V3.4 was developed in the first half of 1987.
-
-Thierry Coquand held a post-doctoral position in Cambrige University
-in 1986-87, where he developed a variant implementation in SML, with
-which he wrote some developments on fixpoints in Scott's domains.
-
-Version 4
----------
-
-This version saw the beginning of program extraction from proofs, with
-two varieties of the type `Prop` of propositions, indicating
-constructive intent.  The proof extraction algorithms were implemented
-by Christine Paulin-Mohring.
-
-V4.1 was frozen on July 24th, 1987. It had a first identified library
-of mathematical developments (directory exemples), with libraries
-Logic (containing impredicative encodings of intuitionistic logic and
-algebraic primitives for booleans, natural numbers and list), `Peano`
-developing second-order Peano arithmetic, `Arith` defining addition,
-multiplication, euclidean division and factorial. Typical developments
-were the Knaster-Tarski theorem and Newman's lemma from rewriting
-theory.
-
-V4.2 was a joint development of a team consisting of Thierry Coquand,
-Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the
-log of changes.  It was frozen on September 1987 as the last version
-implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable
-development system.
-
-V4.3 saw the first top-level of the system. Instead of evaluating
-explicit quotations, the user could develop his mathematics in a
-high-level language called the mathematical vernacular (following
-Automath terminology).  The user could develop files in the vernacular
-notation (with .v extension) which were now separate from the `ml`
-sources of the implementation.  Gilles Dowek joined the team to
-develop the vernacular language as his DEA internship research.
-
-A notion of sticky constant was introduced, in order to keep names of
-lemmas when local hypotheses of proofs were discharged. This gave a
-notion of global mathematical environment with local sections.
-
-Another significant practical change was that the system, originally
-developped on the VAX central computer of our lab, was transferred on
-SUN personal workstations, allowing a level of distributed
-development.  The extraction algorithm was modified, with three
-annotations `Pos`, `Null` and `Typ` decorating the sorts `Prop` and
-`Type`.
-
-Version 4.3 was frozen at the end of November 1987, and was
-distributed to an early community of users (among those were Hugo
-Herbelin and Loic Colson).
-
-V4.4 saw the first version of (encoded) inductive types.  Now natural
-numbers could be defined as:
-
-[source, coq]
-Inductive NAT : Prop = O : NAT | Succ : NAT->NAT.
-
-These inductive types were encoded impredicatively in the calculus,
-using a subsystem _rec_ due to Christine Paulin.  V4.4 was frozen on
-March 6th 1988.
-
-Version 4.5 was the first one to support inductive types and program
-extraction.  Its banner was _Calcul des Constructions avec
-Réalisations et Synthèse_.  The vernacular language was enriched to
-accommodate extraction commands.
-
-The verification engine design was presented as: G. Huet. _The
-Constructive Engine_. Version 4.5. Invited Conference, 2nd European
-Symposium on Programming, Nancy, March 88.  The final paper,
-describing the V4.9 implementation, appeared in: A perspective in
-Theoretical Computer Science, Commemorative Volume in memory of Gift
-Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.
-
-Version 4.5 was demonstrated in June 1988 at the YoP Institute on
-Logical Foundations of Functional Programming organized by Gérard Huet
-at Austin, Texas.
-
-Version 4.6 was started during the summer of 1988. Its main
-improvement was the complete rehaul of the proof synthesis engine by
-Thierry Coquand, with a tree structure of goals.
-
-Its source code was communicated to Randy Pollack on September 2nd
-1988.  It evolved progressively into LEGO, proof system for Luo's
-formalism of Extended Calculus of Constructions.
-
-The discharge tactic was modified by Gérard Huet to allow for
-inter-dependencies in discharged lemmas. Christine Paulin improved the
-inductive definition scheme in order to accommodate predicates of any
-arity.
-
-Version 4.7 was started on September 6th, 1988.
-
-This version starts exploiting the CAML notion of module in order to
-improve the modularity of the implementation. Now the term verifier is
-identified as a proper module Machine, which the structure of its
-internal data structures being hidden and thus accessible only through
-the legitimate operations.  This machine (the constructive engine) was
-the trusted core of the implementation. The proof synthesis mechanism
-was a separate proof term generator. Once a complete proof term was
-synthesized with the help of tactics, it was entirely re-checked by
-the engine. Thus there was no need to certify the tactics, and the
-system took advantage of this fact by having tactics ignore the
-universe levels, universe consistency check being relegated to the
-final type-checking pass. This induced a certain puzzlement in early
-users who saw, after a successful proof search, their `QED` followed
-by silence, followed by a failure message due to a universe
-inconsistency…
-
-The set of examples comprise set theory experiments by Hugo Herbelin,
-and notably the Schroeder-Bernstein theorem.
-
-Version 4.8, started on October 8th, 1988, saw a major
-re-implementation of the abstract syntax type `constr`, separating
-variables of the formalism and metavariables denoting incomplete terms
-managed by the search mechanism.  A notion of level (with three values
-`TYPE`, `OBJECT` and `PROOF`) is made explicit and a type judgement
-clarifies the constructions, whose implementation is now fully
-explicit. Structural equality is speeded up by using pointer equality,
-yielding spectacular improvements. Thierry Coquand adapts the proof
-synthesis to the new representation, and simplifies pattern matching
-to first-order predicate calculus matching, with important performance
-gain.
-
-A new representation of the universe hierarchy is then defined by
-Gérard Huet.  Universe levels are now implemented implicitly, through
-a hidden graph of abstract levels constrained with an order relation.
-Checking acyclicity of the graph insures well-foundedness of the
-ordering, and thus consistency. This was documented in a memo _Adding
-Type:Type to the Calculus of Constructions_ which was never published.
-
-The development version is released as a stable 4.8 at the end of
-1988.
-
-Version 4.9 is released on March 1st 1989, with the new ``elastic''
-universe hierarchy.
-
-The spring of 1989 saw the first attempt at documenting the system
-usage, with a number of papers describing the formalism:
-
-- _Metamathematical Investigations of a Calculus of Constructions_, by
-  Thierry Coquand <<C90>>,
-- _Inductive definitions in the Calculus of Constructions_, by
-   Christine Paulin-Mohrin,
-- _Extracting Fω's programs from proofs in the Calculus of
-  Constructions_, by Christine Paulin-Mohring <<P89>>,
-- _The Constructive Engine_, by Gérard Huet <<H89>>,
-
-as well as a number of user guides:
-
-- _A short user's guide for the Constructions_ Version 4.10, by Gérard Huet
-- _A Vernacular Syllabus_, by Gilles Dowek.
-- _The Tactics Theorem Prover, User's guide_, Version 4.10, by Thierry
-  Coquand.
-
-Stable V4.10, released on May 1st, 1989, was then a mature system,
-distributed with CAML V2.6.
-
-In the mean time, Thierry Coquand and Christine Paulin-Mohring had
-been investigating how to add native inductive types to the Calculus
-of Constructions, in the manner of Per Martin-Löf's Intuitionistic
-Type Theory. The impredicative encoding had already been presented in:
-F. Pfenning and C. Paulin-Mohring. __Inductively defined types in the
-Calculus of Constructions__ <<PP90>>. An extension of the calculus
-with primitive inductive types appeared in: Th. Coquand and
-C. Paulin-Mohring. __Inductively defined types__ <<CP90>>.
-
-This led to the Calculus of Inductive Constructions, logical formalism
-implemented in Versions 5 upward of the system, and documented in:
-C. Paulin-Mohring. __Inductive Definitions in the System Coq - Rules
-and Properties__ <<P93>>.
-
-The last version of CONSTR is Version 4.11, which was last distributed
-in the spring of 1990. It was demonstrated at the first workshop of
-the European Basic Research Action Logical Frameworks In Sophia
-Antipolis in May 1990.
-
-At the end of 1989, Version 5.1 was started, and renamed as the system
-Coq for the Calculus of Inductive Constructions. It was then ported to
-the new stand-alone implementation of ML called Caml-light.
-
-In 1990 many changes occurred. Thierry Coquand left for Chalmers
-University in Göteborg. Christine Paulin-Mohring took a CNRS
-researcher position at the LIP laboratory of École Normale Supérieure
-de Lyon. Project Formel was terminated, and gave rise to two teams:
-Cristal at INRIA-Roquencourt, that continued developments in
-functional programming with Caml-light then Ocaml, and Coq, continuing
-the type theory research, with a joint team headed by Gérard Huet at
-INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory
-of CNRS-ENS Lyon.
-
-Chetan Murthy joined the team in 1991 and became the main software
-architect of Version 5. He completely rehauled the implementation for
-efficiency.  Versions 5.6 and 5.8 were major distributed versions,
-with complete documentation and a library of users' developements. The
-use of the RCS revision control system, and systematic ChangeLog
-files, allow a more precise tracking of the software developments.
-
-Developments from Version 6 upwards are documented in the credits
-section of Coq's Reference Manual.
-
-====
-September 2015 +
-Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.
-====
-
-[bibliography]
-.Bibliographic references
-
-- [[[CH85]]] Th. Coquand, G. Huet. _Constructions: A Higher Order
-  Proof System for Mechanizing Mathematics_. Invited paper, EUROCAL85,
-  April 1985, Linz, Austria. Springer Verlag LNCS 203, pp. 151-184.
-
-- [[[CH88]]] T. Coquand and G. Huet. _The Calculus of Constructions_.
-  Submitted on June 30th 1985, accepted on December 5th, 1985,
-  Information and Computation. Preprint as Rapport de Recherche Inria
-  n°530, Mai 1986. Final version in Information and Computation
-  76,2/3, Feb. 88.
-
-- [[[CH87]]] Th. Coquand, G. Huet. _Concepts Mathématiques et
-  Informatiques Formalisés dans le Calcul des Constructions_. Invited
-  paper, European Logic Colloquium, Orsay, July 1985. Preprint as
-  Rapport de recherche INRIA n°463, Dec. 85.  Published in Logic
-  Colloquium 1985, North-Holland, 1987.
-
-- [[[P86]]] C. Paulin. _Algorithm development in the Calculus of
-  Constructions_, preprint as Rapport de recherche INRIA n°497,
-  March 86. Final version in Proceedings Symposium on Logic in Computer
-  Science, Cambridge, MA, 1986 (IEEE Computer Society Press).
-
-- [[[H88]]] G. Huet. _Induction Principles Formalized in the Calculus
-  of Constructions_ in Programming of Future Generation Computers,
-  Ed. K. Fuchi and M. Nivat, North-Holland, 1988.
-
-- [[[C90]]] Th. Coquand. _Metamathematical Investigations of a
-  Calculus of Constructions_, by INRIA Research Report N°1088,
-  Sept. 1989, published in Logic and Computer Science,
-  ed. P.G. Odifreddi, Academic Press, 1990.
-
-- [[[P89]]] C. Paulin. _Extracting F ω's programs from proofs in the
-  calculus of constructions_. 16th Annual ACM Symposium on Principles
-  of Programming Languages, Austin. 1989.
-
-- [[[H89]]] G. Huet. _The constructive engine_. A perspective in
-  Theoretical Computer Science. Commemorative Volume for Gift
-  Siromoney. World Scientific Publishing (1989).
-
-- [[[PP90]]] F. Pfenning and C. Paulin-Mohring. _Inductively defined
-  types in the Calculus of Constructions_. Preprint technical report
-  CMU-CS-89-209, final version in Proceedings of Mathematical
-  Foundations of Programming Semantics, volume 442, Lecture Notes in
-  Computer Science. Springer-Verlag, 1990
-
-- [[[CP90]]] Th. Coquand and C. Paulin-Mohring. _Inductively defined
-  types_.  In P. Martin-Löf and G. Mints, editors, Proceedings of
-  Colog'88, volume 417, Lecture Notes in Computer Science.
-  Springer-Verlag, 1990.
-
-- [[[P93]]] C. Paulin-Mohring. _Inductive Definitions in the System
-  Coq - Rules and Properties_. In M. Bezem and J.-F. Groote, editors,
-  Proceedings of the conference Typed Lambda Calculi and Applications,
-  volume 664, Lecture Notes in Computer Science, 1993.
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index a31ab1c511..b1bfac8cc9 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -126,9 +126,9 @@ script again] This will be fixed in the future.
 
 ## Dropping from coqtop:
 
-The following sequence is recommended:
+After doing `make -f Makefile.dune voboot`, the following commands should work:
 ```
-dune exec coqtop.byte
+dune exec dev/shim/coqbyte-prelude
 > Drop.
 # #directory "dev";;
 # #use "include_dune";;
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index e7d4b605c7..491a75bb3d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -72,6 +72,12 @@ Libobject
   * `Libobject.superglobal_object`
   * `Libobject.superglobal_object_nodischarge`
 
+Implicit Arguments
+
+- `Impargs.declare_manual_implicits` is restricted to only support declaration
+  of implicit binders at constant declaration time. `Impargs.set_implicits` should
+  be used for redeclaration of implicit arguments.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
diff --git a/dev/shim/dune b/dev/shim/dune
index 85a0d205da..39b4ef492c 100644
--- a/dev/shim/dune
+++ b/dev/shim/dune
@@ -11,6 +11,19 @@
     (run chmod +x %{targets})))))
 
 (rule
+ (targets coqbyte-prelude)
+ (deps
+  %{bin:coqtop.byte}
+  %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so}
+  %{project_root}/theories/Init/Prelude.vo)
+ (action
+  (with-outputs-to %{targets}
+   (progn
+    (echo "#!/usr/bin/env bash\n")
+    (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+    (run chmod +x %{targets})))))
+
+(rule
  (targets coqide-prelude)
  (deps
   %{bin:coqqueryworker.opt}