27 files changed, 276 insertions, 206 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index c75acb0560..577ce35aae 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -420,6 +420,7 @@ copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOT
 ECHO ========== BUILD COQ ==========
 
 MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+RMDIR /S /Q "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
 MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
 
 COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 87122e0fb5..608cc127a0 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -209,7 +209,7 @@
 ########################################################################
 # bedrock2
 ########################################################################
-: "${bedrock2_CI_REF:=master}"
+: "${bedrock2_CI_REF:=tested}"
 : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}"
 : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}"
 
@@ -256,6 +256,13 @@
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
 
 ########################################################################
+# reduction-effects
+########################################################################
+: "${reduction_effects_CI_REF:=master}"
+: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}"
+: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}"
+
+########################################################################
 # menhirlib
 ########################################################################
 : "${menhirlib_CI_REF:=master}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index 2af4b58201..9ce5da9f50 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -6,8 +6,8 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download fiat_crypto_legacy
 
-fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
-fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded"
+fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
   ./etc/ci/remove_autogenerated.sh && \
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 000c418137..811fefda35 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,11 +9,15 @@ git_download fiat_crypto
 # We need a larger stack size to not overflow ocamlopt+flambda when
 # building the executables.
 # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
+fiat_crypto_CI_STACKSIZE=32768
 
-fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1"
+# fiat-crypto is not guaranteed to build with the latest version of
+# bedrock2, so we use the pinned version of bedrock2, but the external
+# version of other developments
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
 fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
 fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
-        ulimit -s 32768 && \
+        ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
         make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh
new file mode 100755
index 0000000000..6b6de3fa2f
--- /dev/null
+++ b/dev/ci/ci-reduction_effects.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download reduction_effects
+
+( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install)
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 2b1d2298f2..b9d6215e60 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -4,7 +4,10 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2
-data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
+
+# "latest" is disabled due to lack of build credits upstream, thus artifacts fail
+# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
+data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
 
 mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}"
 
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index a9cc91170f..f08a08531f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -60,9 +60,23 @@ let iris = (coqPackages.iris.override { inherit coq stdpp; })
 
 let unicoq = callPackage ./unicoq { inherit coq; }; in
 
+let StructTact = coqPackages.StructTact.overrideAttrs (o: {
+    src = fetchTarball "https://github.com/uwplse/StructTact/tarball/master";
+  }); in
+
+let Cheerios = (coqPackages.Cheerios.override { inherit StructTact; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/uwplse/cheerios/tarball/master";
+  }); in
+
+let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/uwplse/verdi/tarball/master";
+  }); in
+
 let callPackage = newScope { inherit coq
   bignums coq-ext-lib coqprime corn iris math-classes
-  mathcomp simple-io ssreflect stdpp unicoq;
+  mathcomp simple-io ssreflect stdpp unicoq Verdi;
 }; in
 
 # Environments for building CI libraries with this Coq
@@ -89,6 +103,7 @@ let projects = {
   mtac2 = callPackage ./mtac2.nix {};
   oddorder = callPackage ./oddorder.nix {};
   quickchick = callPackage ./quickchick.nix {};
+  verdi-raft = callPackage ./verdi-raft.nix {};
   VST = callPackage ./VST.nix {};
 }; in
 
diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix
index 0f0ee91387..1105fba7a6 100644
--- a/dev/ci/nix/fiat_crypto.nix
+++ b/dev/ci/nix/fiat_crypto.nix
@@ -1,6 +1,6 @@
-{ coqprime }:
+{ ocamlPackages }:
 {
-  coqBuildInputs = [ coqprime ];
+  buildInputs = with ocamlPackages; [ ocaml findlib ];
   configure = "git submodule update --init --recursive && ulimit -s 32768";
-  make = "make new-pipeline c-files";
+  make = "make c-files printlite lite && make -j 1 coq";
 }
diff --git a/dev/ci/nix/verdi-raft.nix b/dev/ci/nix/verdi-raft.nix
new file mode 100644
index 0000000000..6a98f4ef47
--- /dev/null
+++ b/dev/ci/nix/verdi-raft.nix
@@ -0,0 +1,5 @@
+{ Verdi }:
+{
+  coqBuildInputs = [ Verdi ];
+  configure = "./configure";
+}
diff --git a/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh
new file mode 100644
index 0000000000..f41271804a
--- /dev/null
+++ b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11338" ] || [ "$CI_BRANCH" = "rm-global-uses-evd" ]; then
+
+    unicoq_CI_REF=rm-global-uses-evd
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+    equations_CI_REF=rm-global-uses-evd
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
new file mode 100644
index 0000000000..a125337dd9
--- /dev/null
+++ b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
@@ -0,0 +1,33 @@
+if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then
+
+    mathcomp_CI_REF=non_maximal_implicit
+    mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp
+
+    oddorder_CI_REF=non_maximal_implicit
+    oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order
+
+    stdlib2_CI_REF=non_maximal_implicit
+    stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2
+
+    coq_dpdgraph_CI_REF=non_maximal_implicit
+    coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph
+
+    vst_CI_REF=non_maximal_implicit
+    vst_CI_GITURL=https://github.com/SimonBoulier/VST
+
+    equations_CI_REF=non_maximal_implicit
+    equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations
+
+    mtac2_CI_REF=non_maximal_implicit
+    mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2
+
+    relation_algebra_CI_REF=non_maximal_implicit
+    relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra
+
+    fiat_parsers_CI_REF=non_maximal_implicit
+    fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat
+
+    Corn_CI_REF=non_maximal_implicit
+    Corn_CI_GITURL=https://github.com/SimonBoulier/corn
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
deleted file mode 100644
index 66f5a96802..0000000000
--- a/dev/doc/MERGING.md
+++ /dev/null
@@ -1,177 +0,0 @@
-# Merging changes in 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
-
-The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of
-the code. Sometime there is one principal maintainer and one or several
-secondary maintainer(s). Sometimes, it is a team of code owners and all of its
-members act as principal maintainers for the component.
-
-When a PR is submitted, GitHub will automatically ask the principal
-maintainer (or the code owner team) for a review. If the PR touches several
-parts, all the corresponding owners will be asked for a review.
-
-Maintainers are never assigned as reviewer on their own PRs.
-
-If a principal maintainer submits a PR or is a co-author of a PR that is
-submitted and this PR changes the component they own, they must request a
-review from a secondary maintainer. They can also delegate the review if they
-know they are not available to do it.
-
-## Reviewing
-
-When maintainers receive a review request, they are expected to:
-
-* Put their name in the assignee field, if they are in charge of the component
-  that is the main target of the patch (or if they are the only maintainer asked
-  to review the PR).
-* Review the PR, approve it or request changes.
-* If they are the assignee, check if all reviewers approved the PR. If not,
-  regularly ping the author (if changes should be implemented) or the reviewers
-  (if reviews are missing). The assignee ensures that any requests for more
-  discussion have been granted. When the discussion has converged and ALL
-  REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
-  process described below.
-
-To know what files you are a code owner of in a large PR, you can run
-`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect.
-
-When a PR received lots of comments or if the PR has not been opened for long
-and the assignee thinks that some other developers might want to comment,
-it is recommended that they announce their intention to merge and wait a full
-working day (or more if deemed useful) before the actual merge, as a sort of
-last call for comments.
-
-In all cases, maintainers can delegate reviews to the other maintainers,
-except if it would lead to a maintainer reviewing their own patch.
-
-A maintainer is expected to be reasonably reactive, but no specific timeframe is
-given for reviewing.
-
-When none of the maintainers have commented nor self-assigned a PR in a delay
-of five working days, any maintainer of another component who feels comfortable
-reviewing the PR can assign it to themselves. To prevent misunderstandings,
-maintainers should not hesitate to announce in advance when they shall be
-unavailable for more than five working days.
-
-(*) In case a component is touched in a trivial way (adding/removing one file in
-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 from every code owner 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](../ci/README.md#Breaking-changes) and the PR can be tested
-with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
-
-Moreover the PR author *must* add an entry to the [unreleased
-changelog](../../doc/changelog/README.md) or to the
-[`dev/doc/changes.md`](changes.md) 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
-completed without relevant failures, and that the PR comes with appropriate
-documentation and test cases. If not, they should leave a comment on the PR and
-put the appropriate label. Otherwise, they are expected to merge the PR using the
-[merge script](../tools/merge-pr.sh).
-
-When CI has a few failures which look spurious, restarting the corresponding
-jobs is a good way of ensuring this was indeed the case.
-To restart a job on AppVeyor, you should connect using your GitHub
-account; being part of the Coq organization on GitHub should give you the
-permission to do so.
-To restart a job on GitLab CI, you should sign into GitLab (this can be done
-using a GitHub account); if you are part of the
-[Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry"
-button; otherwise, send a request to join the organization.
-
-When the PR has conflicts, the assignee can either:
-- ask the author to rebase the branch, fixing the conflicts
-- warn the author that they are going to rebase the branch, and push to the
-  branch directly
-
-In both cases, CI should be run again.
-
-In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR
-is not a candidate for backporting), it is ok to fix
-the conflicts in the merge commit (following the same steps as below), and push
-to `master` directly. DON'T USE the GitHub interface to fix these conflicts.
-
-To merge the PR proceed in the following way
-```
-$ git checkout master
-$ git pull
-$ dev/tools/merge-pr.sh XXXX
-$ git push upstream
-```
-where `XXXX` is the number of the PR to be merged and `upstream` is the name
-of your remote pointing to `git@github.com:coq/coq.git`.
-Note that you are only supposed to merge PRs into `master`. PRs should rarely
-target the stable branch, but when it is the case they are the responsibility
-of the release manager.
-
-This script conducts various checks before proceeding to merge. Don't bypass them
-without a good reason to, and in that case, write a comment in the PR thread to
-explain the reason.
-
-Maintainers MUST NOT merge their own patches.
-
-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.
-
-### Merge script dependencies
-
-The merge script passes option `-S` to `git merge` to ensure merge commits
-are signed. Consequently, it depends on the GnuPG command utility being
-installed and a GPG key being available. Here is a short documentation on
-how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/.
-
-The script depends on a few other utilities. If you are a Nix user, the
-simplest way of getting them is to run `nix-shell` first.
-
-**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG
-is not out of the box. Installing explicitly "pinentry-mac" seems important for
-typing of passphrase to work correctly (see also this
-[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)).
-
-## Addendum for organization admins
-
-### Adding a new code owner individual
-
-If someone is added to the [`CODEOWNERS`](../../.github/CODEOWNERS) file and
-they did not have merging rights before, they should also be added to the
-**@coq/pushers** team. You may do so using
-[this link](https://github.com/orgs/coq/teams/pushers/members?add=true).
-
-Before adding someone to the **@coq/pushers** team, you should ensure that they
-have read the present merging documentation, and explicitly tell them not to
-use the merging button on the GitHub web interface.
-
-### Adding a new code owner team
-
-Go to [that page](https://github.com/orgs/coq/teams/pushers/teams) and click on
-the green "Add a team" button. Use a "-maintainer" suffix for the name of your
-team. You may then add new members to this team (you don't need to add them to
-the **@coq/pushers** team first as this will be done automatically because the
-team you created is a sub-team of **@coq/pushers**).
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 37c6e2f619..cd35064b18 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -108,24 +108,44 @@ automatically.
 You can use `ocamldebug` with Dune; after a build, do:
 
 ```
-dune exec -- dev/dune-dbg /path/to/foo.v
+dune exec -- dev/dune-dbg coqc foo.v
 (ocd) source dune_db
 ```
 
-or
+to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`:
 
 ```
-dune exec -- dev/dune-dbg checker Foo
+dune exec -- dev/dune-dbg checker foo.vo
 (ocd) source dune_db
 ```
 
-for the checker. Unfortunately, dependency handling here is not fully
-refined, so you need to build enough of Coq once to use this target
-[it will then correctly compute the deps and rebuild if you call the
-script again] This will be fixed in the future.
+Unfortunately, dependency handling here is not fully refined, so you
+need to build enough of Coq once to use this target [it will then
+correctly compute the deps and rebuild if you call the script again]
+This will be fixed in the future.
 
 For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`.
 
+**Note**: If you are using OCaml >= 4.08 you need to use
+
+```
+(ocd) source dune_db_408
+```
+
+or
+
+```
+(ocd) source dune_db_409
+```
+
+depending on your OCaml version. This is due to several factors:
+
+- OCaml >= 4.08 doesn't allow doubly-linking modules, however `source`
+  is not re entrant and seems to doubly-load in the default setup, see
+  https://github.com/coq/coq/issues/8952
+- OCaml >= 4.09 comes with `dynlink` already linked in so we need to
+  modify the list of modules loaded.
+
 ## Dropping from coqtop:
 
 After doing `make -f Makefile.dune voboot`, the following commands should work:
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 04b20c6889..3bc92e6aee 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,13 @@
 
 ### ML API
 
+Exception handling:
+
+- Coq's custom `Backtrace` module has been removed in favor of OCaml's
+  native backtrace implementation. Please use the functions in
+  `Exninfo.capture` and `iraise` when re-raising inside an exception
+  handler.
+
 Printers:
 
 - Functions such as Printer.pr_lconstr_goal_style_env have been
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 67becb251a..3260040248 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -158,7 +158,7 @@ Universes
   component: universe polymorphism, asynchronous proofs
   summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
   introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
-  impacted released: V8.5-V8.10
+  impacted released versions: V8.5-V8.10
   impacted development branches: none
   impacted coqchk versions: immune
   fixed in: PR#10664
@@ -167,6 +167,19 @@ Universes
   GH issue number: none
   risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
 
+  component: algebraic universes
+  summary: Set+2 was incorrectly simplified to Set+1
+  introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a)
+  impacted released versions: V8.10.0 V8.10.1 V8.10.2
+  impacted coqchk versions: same
+  fixed in: PR#11422
+  found by: Gilbert
+  exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration)
+  GH issue number: see PR
+  risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic
+    universes such that +2 increments do not appear), mild risk from plugins which manipulate
+    algebraic universes.
+
 Primitive projections
 
   component: primitive projections, guard condition
@@ -255,6 +268,18 @@ Conversion machines
   GH issue number: #9925
   risk:
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: broken long multiplication primitive integer emulation layer on 32 bits
+  introduced: e43b176
+  impacted released versions: 8.10.0, 8.10.1, 8.10.2
+  impacted development branches: 8.11
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 4e176a7
+  found by: Soegtrop, Melquiond
+  exploit: test-suite/bugs/closed/bug_11321.v
+  GH issue number: #11321
+  risk: critical, as any BigN computation on 32-bit architectures is wrong
+
   component: "native" conversion machine (translation to OCaml which compiles to native code)
   summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
   introduced: V8.5
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 1c486b024d..ba68501e04 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -75,7 +75,8 @@ in time.
 - [ ] Pin the versions of libraries and plugins in
   `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it
   exists, a branch dedicated to compatibility with the corresponding
-  Coq branch).
+  Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this
+  semi-automatically.
 - [ ] Remove all remaining unmerged feature PRs from the beta milestone.
 - [ ] Start a new project to track PR backporting. The project should
   have a "Request X.X+beta1 inclusion" column for the PRs that were
diff --git a/dev/doc/shield-icon.png b/dev/doc/shield-icon.png
new file mode 100644
index 0000000000..629e51a819
--- /dev/null
+++ b/dev/doc/shield-icon.png
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 0fc0a413ba..fca7b77fc2 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -1,12 +1,11 @@
 # Coq XML Protocol
 
 This document is based on documentation originally written by CJ Bell
-for his [vscoq](https://github.com/siegebell/vscoq/) project.
+for his [vscoq](https://github.com/coq-community/vscoq/) project.
 
 Here, the aim is to provide a "hands on" description of the XML
 protocol that coqtop and IDEs use to communicate. The protocol first appeared 
-with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming 
-versions of Proof General.
+with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces.
 
 A somewhat out-of-date description of the async state machine is
 [documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md).
diff --git a/dev/dune b/dev/dune
index 11e42f97f3..b312a55706 100644
--- a/dev/dune
+++ b/dev/dune
@@ -13,6 +13,8 @@
         ../checker/coqchk.bc
         ../topbin/coqc_bin.bc
         ../ide/coqide_main.bc
-        ; This is not enough as the call to `ocamlfind` will fail :/
+        %{lib:coq.plugins.ltac:ltac_plugin.cma}
+        ; This is not enough, the call to `ocamlfind` may fail if the
+        ; META file is not yet in place :/
         top_printers.cma)
   (action (copy dune-dbg.in dune-dbg)))
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 1382f4d1b6..498f167eb1 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -7,11 +7,21 @@ case $1 in
         exe=_build/default/checker/coqchk.bc
         ;;
     coqide)
+        shift
         exe=_build/default/ide/coqide_main.bc
         ;;
-    *)
+    coqc)
+        shift
         exe=_build/default/topbin/coqc_bin.bc
         ;;
+    coqtop)
+        shift
+        exe=_build/default/topbin/coqtop_byte_bin.bc
+        ;;
+    *)
+        echo "First argument must be one of {coqc,coqtop,checker,coqide}"
+        exit 1
+        ;;
 esac
 
 emacs="${INSIDE_EMACS:+-emacs}"
diff --git a/dev/dune_db_408 b/dev/dune_db_408
new file mode 100644
index 0000000000..3bf13da62d
--- /dev/null
+++ b/dev/dune_db_408
@@ -0,0 +1,25 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer config.cma
+load_printer clib.cma
+load_printer dynlink.cma
+load_printer lib.cma
+load_printer gramlib.cma
+load_printer byterun.cma
+load_printer kernel.cma
+load_printer library.cma
+load_printer engine.cma
+load_printer pretyping.cma
+load_printer interp.cma
+load_printer proofs.cma
+load_printer parsing.cma
+load_printer printing.cma
+load_printer tactics.cma
+load_printer vernac.cma
+load_printer stm.cma
+load_printer toplevel.cma
+
+load_printer ltac_plugin.cma
+load_printer top_printers.cma
+
+source top_printers.dbg
diff --git a/dev/dune_db_409 b/dev/dune_db_409
new file mode 100644
index 0000000000..1267fd5393
--- /dev/null
+++ b/dev/dune_db_409
@@ -0,0 +1,24 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer config.cma
+load_printer clib.cma
+load_printer lib.cma
+load_printer gramlib.cma
+load_printer byterun.cma
+load_printer kernel.cma
+load_printer library.cma
+load_printer engine.cma
+load_printer pretyping.cma
+load_printer interp.cma
+load_printer proofs.cma
+load_printer parsing.cma
+load_printer printing.cma
+load_printer tactics.cma
+load_printer vernac.cma
+load_printer stm.cma
+load_printer toplevel.cma
+
+load_printer ltac_plugin.cma
+load_printer top_printers.cma
+
+source top_printers.dbg
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 224601bbce..553696410c 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -33,6 +33,6 @@ echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
 echo Checking ocamlformat
-dune build @fmt || CODE=1
+make -f Makefile.dune fmt || CODE=1
 
 exit $CODE
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index 677377f868..54baaee1fe 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/f4ad230f90ef312695adc26f256036203e9c70af.tar.gz";
-  sha256 = "0cdd275dz3q51sknn7s087js81zvaj5riz8f29id6j6chnyikzjq";
+  url = "https://github.com/NixOS/nixpkgs/archive/8da81465c19fca393a3b17004c743e4d82a98e4f.tar.gz";
+  sha256 = "1f3s27nrssfk413pszjhbs70wpap43bbjx2pf4zq5x2c1kd72l6y";
 })
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index c0a3eeb11c..a888998ebf 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -137,7 +137,8 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then
     else
         error "Local branch is not up-to-date with ${REMOTE}."
         error "Pull before merging."
-        ask_confirmation
+        # This check should never be bypassed.
+        exit 1
     fi
 fi
 
diff --git a/dev/tools/pin-ci.sh b/dev/tools/pin-ci.sh
new file mode 100755
index 0000000000..dbf54d7f0a
--- /dev/null
+++ b/dev/tools/pin-ci.sh
@@ -0,0 +1,46 @@
+#!/usr/bin/env bash
+
+# Use this script to pin the commit used by the developments tracked by the CI
+
+OVERLAYS="./dev/ci/ci-basic-overlay.sh"
+
+process_development() {
+  local DEV=$1
+  local REPO_VAR="${DEV}_CI_GITURL"
+  local REPO=${!REPO_VAR}
+  local BRANCH_VAR="${DEV}_CI_REF"
+  local BRANCH=${!BRANCH_VAR}
+  if [[ -z "$BRANCH" ]]
+  then
+    echo "$DEV has no branch set, skipping"
+    return 0
+  fi
+  if [[ $BRANCH =~ ^[a-f0-9]{40}$ ]]
+  then
+    echo "$DEV is already set to hash $BRANCH, skipping"
+    return 0
+  fi
+  echo "Resolving $DEV as $BRANCH from $REPO"
+  local HASH=$(git ls-remote --heads $REPO $BRANCH | cut -f 1)
+  if [[ -z "$HASH" ]]
+  then
+    echo "Could not resolve reference $BRANCH for $DEV (something went wrong), skipping"
+    return 0
+  fi
+  read -p "Expand $DEV from $BRANCH to $HASH? [y/N] " -n 1 -r
+  echo
+  if [[ $REPLY =~ ^[Yy]$ ]]; then
+    # use -i.bak to be compatible with MacOS; see, e.g., https://stackoverflow.com/a/7573438/377022
+    sed -i.bak -e "s/$BRANCH_VAR:=$BRANCH/$BRANCH_VAR:=$HASH/" $OVERLAYS
+  fi
+}
+
+# Execute the script to set the overlay variables
+. $OVERLAYS
+
+# Find all variables declared in the base overlay of the form *_CI_GITURL
+for REPO_VAR in $(compgen -A variable | grep _CI_GITURL)
+do
+  DEV=${REPO_VAR%_CI_GITURL}
+  process_development $DEV
+done
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 835c20a4f7..f640a33773 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -254,7 +254,9 @@ let ppenvwithcst e = pp
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
-let ppobj obj = Format.print_string (Libobject.object_tag obj)
+let ppobj obj =
+  let Libobject.Dyn.Dyn (tag, _) = obj in
+  Format.print_string (Libobject.Dyn.repr tag)
 
 let cnt = ref 0