22 files changed, 334 insertions, 94 deletions
diff --git a/dev/base_include b/dev/base_include
index 2f7183dd6..2f5d8aa84 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -231,7 +231,7 @@ let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
   (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
-let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
 let _ =
  print_string
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 3608f7305..ecc45735f 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -847,7 +847,7 @@ function make_ocaml {
 
 function make_ocaml_tools {
   make_findlib
-  make_menhir
+  # make_menhir
   make_camlp5
 }
 
@@ -856,7 +856,7 @@ function make_ocaml_tools {
 function make_ocaml_libs {
   make_findlib
   make_lablgtk
-  make_stdint
+  # make_stdint
 }
 
 ##### FINDLIB Ocaml library manager #####
diff --git a/dev/checker.dbg b/dev/checker.dbg
new file mode 100644
index 000000000..b2323b617
--- /dev/null
+++ b/dev/checker.dbg
@@ -0,0 +1,6 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer clib.cma
+load_printer dynlink.cma
+load_printer lib.cma
+load_printer check.cma
diff --git a/dev/checker_db b/dev/checker_db
new file mode 100644
index 000000000..327e636c5
--- /dev/null
+++ b/dev/checker_db
@@ -0,0 +1,39 @@
+source checker.dbg
+
+load_printer checker_printers.cmo
+
+install_printer Checker_printers.pP
+
+install_printer Checker_printers.ppfuture
+
+install_printer Checker_printers.ppid
+install_printer Checker_printers.pplab
+install_printer Checker_printers.ppmbid
+install_printer Checker_printers.ppdir
+install_printer Checker_printers.ppmp
+install_printer Checker_printers.ppcon
+install_printer Checker_printers.ppproj
+install_printer Checker_printers.ppkn
+install_printer Checker_printers.ppmind
+install_printer Checker_printers.ppind
+
+install_printer Checker_printers.ppbigint
+
+install_printer Checker_printers.ppintset
+install_printer Checker_printers.ppidset
+
+install_printer Checker_printers.ppidmapgen
+
+install_printer Checker_printers.ppididmap
+
+install_printer Checker_printers.ppuni
+install_printer Checker_printers.ppuni_level
+install_printer Checker_printers.ppuniverse_set
+install_printer Checker_printers.ppuniverse_instance
+install_printer Checker_printers.ppauniverse_context
+install_printer Checker_printers.ppuniverse_context
+install_printer Checker_printers.ppconstraints
+install_printer Checker_printers.ppuniverse_context_future
+install_printer Checker_printers.ppuniverses
+
+install_printer Checker_printers.pploc
diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml
new file mode 100644
index 000000000..40ae1a7b0
--- /dev/null
+++ b/dev/checker_printers.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open Names
+open Univ
+
+let pp   x = Pp.pp_with Format.std_formatter x
+
+(** Future printer *)
+
+let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
+
+(* name printers *)
+let ppid id = pp (Id.print id)
+let pplab l = pp (Label.print l)
+let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
+let ppdir dir = pp (DirPath.print dir)
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
+let ppcon con = pp(Constant.debug_print con)
+let ppproj con = pp(Constant.debug_print (Projection.constant con))
+let ppkn kn = pp(str (KerName.to_string kn))
+let ppmind kn = pp(MutInd.debug_print kn)
+let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
+
+(* term printers *)
+let ppbigint n = pp (str (Bigint.to_string n));;
+
+let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
+let ppintset l = pp (prset int (Int.Set.elements l))
+let ppidset l = pp (prset Id.print (Id.Set.elements l))
+
+let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
+
+let pridmap pr l =
+  let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in
+  prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
+let ppidmap pr l = pp (pridmap pr l)
+
+let pridmapgen l =
+  let dom = Id.Set.elements (Id.Map.domain l) in
+  if dom = [] then str "[]" else
+  str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]"
+let ppidmapgen l = pp (pridmapgen l)
+
+let prididmap = pridmap (fun _ -> Id.print)
+let ppididmap = ppidmap (fun _ -> Id.print)
+
+let pP s = pp (hov 0 s)
+
+(* proof printers *)
+let ppuni u = pp(Universe.pr u)
+let ppuni_level u = pp (Level.pr u)
+
+let ppuniverse_set l = pp (LSet.pr l)
+let ppuniverse_instance l = pp (Instance.pr l)
+let ppauniverse_context l = pp (AUContext.pr Level.pr l)
+let ppuniverse_context l = pp (pr_universe_context Level.pr l)
+let ppconstraints c = pp (pr_constraints Level.pr c)
+let ppuniverse_context_future c =
+  let ctx = Future.force c in
+    ppuniverse_context ctx
+let ppuniverses u = pp (Univ.pr_universes u)
+
+let pploc x = let (l,r) = Loc.unloc x in
+  print_string"(";print_int l;print_string",";print_int r;print_string")"
diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli
new file mode 100644
index 000000000..2f9500c5c
--- /dev/null
+++ b/dev/checker_printers.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Printers for the ocaml toplevel. *)
+
+val pp : Pp.t -> unit
+val pP : Pp.t -> unit (* with surrounding box *)
+
+val ppfuture : 'a Future.computation -> unit
+
+val ppid : Names.Id.t -> unit
+val pplab : Names.Label.t -> unit
+val ppmbid : Names.MBId.t -> unit
+val ppdir : Names.DirPath.t -> unit
+val ppmp : Names.ModPath.t -> unit
+val ppcon : Names.Constant.t -> unit
+val ppproj : Names.Projection.t -> unit
+val ppkn : Names.KerName.t -> unit
+val ppmind : Names.MutInd.t -> unit
+val ppind : Names.inductive -> unit
+
+val ppbigint : Bigint.bigint -> unit
+
+val ppintset : Int.Set.t -> unit
+val ppidset : Names.Id.Set.t -> unit
+
+val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t
+val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit
+
+val pridmapgen : 'a Names.Id.Map.t -> Pp.t
+val ppidmapgen : 'a Names.Id.Map.t -> unit
+
+val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t
+val ppididmap : Names.Id.t Names.Id.Map.t -> unit
+
+(* Universes *)
+val ppuni : Univ.Universe.t -> unit
+val ppuni_level : Univ.Level.t -> unit (* raw *)
+val ppuniverse_set : Univ.LSet.t -> unit
+val ppuniverse_instance : Univ.Instance.t -> unit
+val ppauniverse_context : Univ.AUContext.t -> unit
+val ppuniverse_context : Univ.UContext.t -> unit
+val ppconstraints : Univ.Constraint.t -> unit
+val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
+val ppuniverses : Univ.universes -> unit
+
+val pploc : Loc.t -> unit
diff --git a/dev/ci/README.md b/dev/ci/README.md
index dee3d2aff..697a160ca 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -107,19 +107,32 @@ there are some.
 
 You can also run one CI target locally (using `make ci-somedev`).
 
-Whenever your PR breaks tested developments, you should either adapt it
-so that it doesn't, or provide a branch fixing these developments (or at
-least work with the author of the development / other Coq developers to
-prepare these fixes). Then, add an overlay in
-[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there)
-as part of your PR.
+See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
 
-The process to merge your PR is then to submit PRs to the external
-development repositories, merge the latter first (if the fixes are
-backward-compatible), and merge the PR on Coq then.
+### Breaking changes
 
-See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
+When your PR breaks an external project we test in our CI, you must prepare a
+patch (or ask someone to prepare a patch) to fix the project:
+
+1. Fork the external project, create a new branch, push a commit adapting
+   the project to your changes.
+2. Test your pull request with your adapted version of the external project by
+   adding an overlay file to your pull request (cf.
+   [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)).
+3. Fixes to external libraries (pure Coq projects) *must* be backward
+   compatible (i.e. they should also work with the development version of Coq,
+   and the latest stable version). This will allow you to open a PR on the
+   external project repository to have your changes merged *before* your PR on
+   Coq can be integrated.
 
+   On the other hand, patches to plugins (projects linking to the Coq ML API)
+   can very rarely be made backward compatible and plugins we test will
+   generally have a dedicated branch per Coq version.
+   You can still open a pull request but the merging will be requested by the
+   developer who merges the PR on Coq. There are plans to improve this, cf.
+   [#6724](https://github.com/coq/coq/issues/6724).
+
+Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file.
 
 Advanced GitLab CI information
 ------------------------------
@@ -141,7 +154,6 @@ no OCaml warnings build Coq in parallel with other tests.
 
 ### GitLab and Windows
 
-
 If your repository has access to runners tagged `windows`, setting the
 secret variable `WINDOWS` to `enabled` will add jobs building Windows
 versions of Coq (32bit and 64bit).
@@ -155,6 +167,10 @@ System and opam packages are installed in a Docker image. The image is
 automatically built and uploaded to your GitLab registry, and is
 loaded by subsequent jobs.
 
+**IMPORTANT**: When updating Coq's CI docker image, you must modify
+the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`,
+and `Dockerfile`.
+
 The Docker building job reuses the uploaded image if it is available,
 but if you wish to save more time you can skip the job by setting
 `SKIP_DOCKER` to `true`.
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 5d96c2499..feabf72d4 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,5 +9,6 @@ git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypt
 
 ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
 
-fiat_crypto_CI_TARGETS="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
-( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} )
+fiat_crypto_CI_TARGETS1="printlite lite lite-display"
+fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 4fc06e895..6a064b297 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -7,4 +7,4 @@ math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes"
 
 git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}"
 
-( cd "${math_classes_CI_DIR}" && make && make install )
+( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index d04b9637c..2ac4d2167 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -8,6 +8,17 @@ pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop"
 
 git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
 
-( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top )
+# Travis / Gitlab have different filesystem layout due to use of
+# `-local`. We need to improve this divergence but if we use Dune this
+# "local" oddity goes away automatically so not bothering...
+if [ -d "$COQBIN/../lib/coq" ]; then
+   COQOCAMLLIB="$COQBIN/../lib/"
+   COQLIB="$COQBIN/../lib/coq/"
+else
+   COQOCAMLLIB="$COQBIN/../"
+   COQLIB="$COQBIN/../"
+fi
 
-echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop
+( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install )
+
+echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
index 8e677f6f2..919e2a735 100644
--- a/dev/ci/docker/README.md
+++ b/dev/ci/docker/README.md
@@ -1,37 +1,13 @@
 ## Overall Docker Setup for Coq's CI.
 
 This directory provides Docker images to be used by Coq's CI. The
-images do support Docker autobuild on `hub.docker.com`
+images do support Docker autobuild on `hub.docker.com` and Gitlab's
+private registry.
 
-Autobuild is the preferred build method [see below]; if you are a
-member of the `coqci` organization, the automated build will push the
-image to the `coqci/name:$VERSION` tag using a Docker hub hook.
-
-## Updating the Image and Syncronization with CI files
-
-Unfortunately, at this point some manual synchronization is needed
-between the `Dockerfile` and `.gitlab-ci.yml`. In particular, the
-checklist is:
-
-- check the name and version of the image setup in `hooks/post_push`
-  have to match.
-- check `COMPILER` variables do match.
-
-Once you are sure the variables are right, then proceed to trigger an
-autobuild or do a manual build, et voilà !
-
-## Docker Autobuilding.
-
-We provide basic support for auto-building, see:
-
-https://docs.docker.com/docker-cloud/builds/advanced/
-
-If you are member of the `coqci` Docker organization, trigger an
-autobuild in your account and the image will be pushed to it as we
-set the proper tag in `hooks/post_push`.
-
-We still need to figure out how properly setup a more automated,
-organization-wide auto-building process.
+Gitlab CI will build and tag a Docker by default for every job if the
+`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this
+variable is usually set to `false` indeed to avoid booting a useless
+job.
 
 ## Manual Building
 
@@ -47,10 +23,6 @@ To upload/push to your hub:
   + `docker tag base:$VERSION $USER/base:$VERSION`
   + `docker push $USER/base:$VERSION`
 
-Now your docker image is ready to be used. To upload to `coqci`:
-- `docker tag base:$VERSION coqci/base:$VERSION`
-- `docker push coqci/base:$VERSION`
-
 ## Debugging / Misc
 
 To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>`
@@ -62,4 +34,3 @@ end.
 ## Possible Improvements:
 
 - Use ARG for customizing versions, centralize variable setup;
-- Learn more about Docker registry for GITLAB https://gitlab.com/coq/coq/container_registry .
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 689d203a1..a1178ee2a 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,3 +1,6 @@
+# CACHEKEY: "bionic_coq-V2018-05-07-V2"
+# ^^ Update when modifying this file.
+
 FROM ubuntu:bionic
 LABEL maintainer="e@x80.org"
 
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
deleted file mode 100755
index 307680aa5..000000000
--- a/dev/ci/docker/bionic_coq/hooks/post_push
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-COQCI_VERSION=V2018-05-07-V2
-docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION
-docker push $DOCKER_REPO:$COQCI_VERSION
-
-docker tag $IMAGE_NAME coqci/base:$COQCI_VERSION
-docker push coqci/base:$COQCI_VERSION
diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
new file mode 100644
index 000000000..ca0076b46
--- /dev/null
+++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then
+    pidetop_CI_BRANCH=stm+top
+    pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git
+fi
diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
new file mode 100644
index 000000000..ea9cd8ee0
--- /dev/null
+++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then
+
+    # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550
+    #
+    # equations
+    # ltac2
+
+    # The below developments should instead use a backwards compatible fix.
+    #
+    # color
+    # iris-lambda-rust
+    # math-classes
+    # formal-topology
+
+    ltac2_CI_BRANCH=tactics+push_fix_naming_out
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Equations_CI_BRANCH=tactics+push_fix_naming_out
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index a7474e324..aec2dfe0a 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,8 +1,21 @@
 # Add overlays for your pull requests in this directory
 
-An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+When your pull request breaks an external project we test in our CI and you
+have prepared a branch with the fix, you can add an "overlay" to your pull
+request to test it with the adapted version of the external project.
 
-The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+An overlay is a file which defines where to look for the patched version so that
+testing is possible. It redefines some variables from
+[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh):
+give the name of your branch using a `_CI_BRANCH` variable and the location of
+your fork using a `_CI_GITURL` variable.
+
+Moreover, the file contains very simple logic to test the pull request number
+or branch name and apply it only in this case.
+
+The name of your overlay file should start with a five-digit pull request
+number, followed by a dash, anything (for instance your GitHub nickname
+and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
 
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
diff --git a/dev/core.dbg b/dev/core.dbg
index edf67020a..972ba701e 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -2,8 +2,8 @@ source camlp5.dbg
 load_printer threads.cma
 load_printer str.cma
 load_printer clib.cma
-load_printer lib.cma
 load_printer dynlink.cma
+load_printer lib.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index a466124c1..65457b63a 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -1,8 +1,8 @@
 # Merging changes in Coq
 
-This document describes how patches (submitted as pull requests
-on the `master` branch) should be
-merged into the main repository (https://github.com/coq/coq).
+This document describes how patches, submitted as pull requests (PRs) on the
+`master` branch, should be merged into the main repository
+(https://github.com/coq/coq).
 
 ## Code owners
 
@@ -10,8 +10,8 @@ The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
 system, two owners. One is the principal maintainer of the component, the other
 is the secondary maintainer.
 
-When a pull request is submitted, GitHub will automatically ask the principal
-maintainer for a review. If the pull request touches several parts, all the
+When a PR is submitted, GitHub will automatically ask the principal
+maintainer for a review. If the PR touches several parts, all the
 corresponding principal maintainers will be asked for a review.
 
 Maintainers are never assigned as reviewer on their own PRs.
@@ -43,10 +43,31 @@ A maintainer is expected to be reasonably reactive, but no specific timeframe is
 given for reviewing.
 
 (*) In case a component is touched in a trivial way (adding/removing one file in
-a `Makefile`, etc), or by applying a systematic process (global renaming,
-deprecationg propagation, etc) that has been reviewed globally, the assignee can
+a `Makefile`, etc), or by applying a systematic refactoring process (global
+renaming for instance) that has been reviewed globally, the assignee can
 say in a comment they think a review is not required and proceed with the merge.
 
+### Breaking changes
+
+If the PR breaks compatibility of some external projects in CI, then fixes to
+those external projects should have been prepared (cf. the relevant sub-section
+in the [CI README](/dev/ci/README.md#Breaking-changes) and the PR can be tested
+with these fixes thanks to ["overlays"](/dev/ci/user-overlays/README.md).
+
+Moreover the PR must absolutely update the [`CHANGES`](/CHANGES) file.
+
+If overlays are missing, ask the author to prepare them and label the PR with
+the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
+
+When fixes are ready, there are two cases to consider:
+
+- For patches that are backward compatible (best scenario), you should get the
+  external project maintainers to integrate them before merging the PR.
+- For patches that are not backward compatible (which is often the case when
+  patching plugins after an update to the Coq API), you can proceed to merge
+  the PR and then notify the external project maintainers they can merge the
+  patch.
+
 ## Merging
 
 Once all reviewers approved the PR, the assignee is expected to check that CI
@@ -89,22 +110,6 @@ DON'T USE the GitHub interface for merging, since it will prevent the automated
 backport script from operating properly, generates bad commit messages, and a
 messy history when there are conflicts.
 
-### What to do if the PR has overlays
-
-If the PR breaks compatibility of some developments in CI, then the author must
-have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md))
-and the PR must absolutely update the `CHANGES` file.
-
-There are two cases to consider:
-
-- If the patch is backward compatible (best scenario), then you should get
-  upstream maintainers to integrate it before merging the PR.
-- If the patch is not backward compatible (which is often the case when
-  patching plugins after an update to the Coq API), then you can proceed to
-  merge the PR and then notify upstream they can merge the patch. This is a
-  less preferable scenario because it is probably going to create
-  spurious CI failures for unrelated PRs.
-
 ### Merge script dependencies
 
 The merge script passes option `-S` to `git merge` to ensure merge commits
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fb3f751db..774a77c8a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,12 @@
 
 ### ML API
 
+Misctypes
+
+  Syntax for universe sorts and kinds has been moved from `Misctypes`
+  to `Glob_term`, as these are turned into kernel terms by
+  `Pretyping`.
+
 Proof engine
 
 - More functions have been changed to use `EConstr`, notably the
@@ -22,6 +28,13 @@ Proof engine
   should indicate what the canonical form is. An important change is
   the move of `Globnames.global_reference` to `Names.GlobRef.t`.
 
+ML Libraries used by Coq
+
+- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
+  Array.Smart.map.
+- Uniformization of some names, e.g. Array.Smart.fold_left_map instead
+  of Array.smartfoldmap.
+
 ### Unit testing
 
   The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 8f1c165dd..2bec09de2 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -14,7 +14,15 @@
 
 export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
 
-exec $OCAMLDEBUG \
+GUESS_CHECKER=
+for arg in "$@"; do
+    if [ "${arg##*/}" = coqchk.byte ]; then
+        GUESS_CHECKER=1
+    fi
+done
+
+if [ -z "$GUESS_CHECKER" ]; then
+    exec $OCAMLDEBUG \
 	-I $CAMLP5LIB -I +threads \
 	-I $COQTOP \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
@@ -35,3 +43,11 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
         -I $COQTOP/ide \
 	"$@"
+else
+    exec $OCAMLDEBUG \
+        -I $CAMLP5LIB -I +threads \
+        -I $COQTOP \
+        -I $COQTOP/config -I $COQTOP/clib \
+        -I $COQTOP/lib -I $COQTOP/checker \
+        "$@"
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8d5b5bef4..cb1abc4a9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -203,17 +203,17 @@ let pproof p = pp(Proof.pr_proof p)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let prlev = Universes.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes
 let ppuniverse_set l = pp (LSet.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prlev l)
 let ppuniverse_context l = pp (pr_universe_context prlev l)
 let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
-let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
+let ppuniverse_opt_subst l = pp (UnivSubst.pr_universe_opt_subst l)
 let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
 let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l)
 let ppconstraints c = pp (pr_constraints Level.pr c)
-let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
+let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index c23ba964c..63d7d5805 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -139,11 +139,11 @@ val ppuniverse_instance : Univ.Instance.t -> unit
 val ppuniverse_context : Univ.UContext.t -> unit
 val ppuniverse_context_set : Univ.ContextSet.t -> unit
 val ppuniverse_subst : Univ.universe_subst -> unit
-val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit
+val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit
 val ppuniverse_level_subst : Univ.universe_level_subst -> unit
 val ppevar_universe_context : UState.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
-val ppuniverseconstraints : Universes.Constraints.t -> unit
+val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
 val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
 val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit