22 files changed, 238 insertions, 199 deletions
diff --git a/dev/base_include b/dev/base_include
index daee2d97c5..f375a867bc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -134,7 +134,6 @@ open ComDefinition
 open Indschemes
 open Ind_tables
 open Auto_ind_decl
-open Coqinit
 open Coqtop
 open Himsg
 open Metasyntax
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml
index 25545cf565..69136ee773 100644
--- a/dev/bench/gitlab-bench.yml
+++ b/dev/bench/gitlab-bench.yml
@@ -4,9 +4,7 @@ bench:
   when: manual
   before_script:
     - printenv -0 | sort -z | tr '\0' '\n'
-  script:
-    - . ~/.opam/opam-init/init.sh
-    - ./dev/bench/gitlab.sh
+  script: dev/bench/gitlab.sh
   tags:
     - timing
   variables:
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index b616371ef8..569977f76b 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -52,7 +52,7 @@ check_variable "CI_JOB_URL"
 : "${new_coq_opam_archive_git_branch:=master}"
 : "${old_coq_opam_archive_git_branch:=master}"
 : "${num_of_iterations:=1}"
-: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial}"
+: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial coq-vst}"
 
 new_coq_commit=$(git rev-parse HEAD^2)
 old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit)
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index b4b6411d28..8f14625c63 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -44,7 +44,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages
 ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
     CI_OPAM="ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.12.0"
+    BASE_ONLY_OPAM="elpi.1.13.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
diff --git a/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh b/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh
new file mode 100644
index 0000000000..d80363c49f
--- /dev/null
+++ b/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi debug-infra 13202
diff --git a/dev/ci/user-overlays/13842-proux01-remove-decimal.sh b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh
new file mode 100644
index 0000000000..5ede8221ce
--- /dev/null
+++ b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh
@@ -0,0 +1 @@
+overlay hott https://github.com/proux01/HoTT coq-13842 13842
diff --git a/dev/ci/user-overlays/13844-gares-command-loc.sh b/dev/ci/user-overlays/13844-gares-command-loc.sh
new file mode 100644
index 0000000000..d9a1736532
--- /dev/null
+++ b/dev/ci/user-overlays/13844-gares-command-loc.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/LPCIC/coq-elpi command-loc 13844
diff --git a/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh b/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh
new file mode 100644
index 0000000000..6847bde6d8
--- /dev/null
+++ b/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.0 13847
diff --git a/dev/core.dbg b/dev/core.dbg
index 6d52bae773..dcf9910b0b 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -16,5 +16,6 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
index 3f73cf126a..da3022644d 100644
--- a/dev/core_dune.dbg
+++ b/dev/core_dune.dbg
@@ -17,5 +17,6 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 79c2155823..4452baf513 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -332,6 +332,18 @@ Conversion machines
   GH issue number: ocaml/ocaml#6385, #11170
   risk: unlikely to be activated by chance, might happen for autogenerated code
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: buffer overflow, arbitrary code execution on floating-point operations
+  introduced: 8.13
+  impacted released versions: 8.13.0
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 8.13.1
+  found by: Melquiond
+  GH issue number: #13867
+  risk: none, unless using floating-point operations; high otherwise;
+        noticeable if activated by chance, since it usually breaks
+        control-flow integrity
+
 Side-effects
 
   component: side-effects
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 19562b60a2..57c325f698 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -1,176 +1,162 @@
-# Release process #
-
-## As soon as the previous version branched off master ##
-
-In principle, these steps should be undertaken by the RM of the next
-release. Unfortunately, we have not yet been able to nominate RMs
-early enough in the process for this person to be known at that point
-in time.
-
-- [ ] Create a new issue to track the release process where you can copy-paste
-  the present checklist from `dev/doc/release-process.md`.
-- [ ] Change the version name to the next major version and the magic
-  numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)).
+# Release checklist #
+
+## When the release managers for version `X.X` get nominated ##
+
+- [ ] Create a new issue to track the release process where you can
+  copy-paste the present checklist from `dev/doc/release-process.md`.
+- [ ] Decide the release calendar with the team (date of branching,
+  preview and final release).
+- [ ] Create a wiki page that you link to from
+  https://github.com/coq/coq/wiki/Release-Plan with this information
+  and the link to the issue.
+
+## About one month before the branching date ##
+
+- [ ] Create both the upcoming final release (`X.X.0`) and the
+  following major release (`Y.Y+rc1`) milestones if they do not
+  already exist.
+- [ ] Send an announcement of the upcoming branching date on Coqdev +
+  the Coq development category on Discourse (coqdev@inria.fr +
+  coq+coq-development@discoursemail.com) and ask people to remove from
+  the `X.X+rc1` milestone any feature and clean up PRs that they
+  already know won't be ready on time.
+- [ ] In a PR on `master`, call
+  [`dev/tools/update-compat.py`](../tools/update-compat.py) with the
+  `--release` flag; this sets up Coq to support three `-compat` flag
+  arguments including the upcoming one (instead of four).  To ensure
+  that CI passes, you will have to decide what to do about all
+  test-suite files which mention `-compat U.U` or `Coq.Comapt.CoqUU`
+  (which is no longer valid, since we only keep compatibility against
+  the two previous versions), and you may have to ping maintainers of
+  projects that are still relying on the old compatibility flag so
+  that they fix this.
+- [ ] Make sure that this change is merged in time for the branching
+  date.
+
+## On the branching date ##
+
+- [ ] In a PR on `master`, change the version name to the next major
+  version and the magic numbers (see
+  [#7008](https://github.com/coq/coq/pull/7008/files)).
 
   Additionally, in the same commit, update the compatibility
   infrastructure, which consists of invoking
   [`dev/tools/update-compat.py`](../tools/update-compat.py) with the
   `--master` flag.
 
-  Note that the `update-compat.py` script must be run twice: once
-  *immediately after* branching with the `--master` flag (which sets
-  up Coq to support four `-compat` flag arguments), *in the same
-  commit* as the one that updates `coq_version` in
-  [`configure.ml`](../../configure.ml), and once again later on before
-  the next branch point with the `--release` flag (see next section).
-- [ ] Put the corresponding alpha tag using `git tag -s`.
-  The `VX.X+alpha` tag marks the first commit to be in `master` and not in the
-  branch of the previous version. Note that this commit is the first commit
+  Note that the `update-compat.py` script must be run twice: once in
+  preparation of the release with the `--release` flag (see previous
+  section) and once on the branching date with the `--master` flag to
+  mark the start of the next version.
+- [ ] Merge the above PR and create the `vX.X` branch from the last
+  merge commit before this one (using this name will ensure that the
+  branch will be automatically protected).
+- [ ] Set the next major version alpha tag using `git tag -s`.  The
+  `VY.Y+alpha` tag marks the first commit to be in `master` and not in
+  the `vX.X` release branch. Note that this commit is the first commit
   in the first PR merged in master, not the merge commit for that PR.
-  After tagging double check that `git describe` picks up
-  the tag you just made (if not, you tagged the wrong commit).
-- [ ] Create the `X.X+beta1` milestone if it did not already exist.
-- [ ] Decide the release calendar with the team (freeze date, beta date, final
-  release date) and put this information in the milestone (using the
-  description and due date fields).
-
-## Anytime after the previous version is branched off master ##
-
-- [ ] Update the compatibility infrastructure to the next release,
-  which consists of invoking
-  [`dev/tools/update-compat.py`](../tools/update-compat.py) with the
-  `--release` flag; this sets up Coq to support three `-compat` flag
-  arguments.  To ensure that CI passes, you will have to decide what
-  to do about all test-suite files which mention `-compat U.U` or
-  `Coq.Comapt.CoqUU` (which is no longer valid, since we only keep
-  compatibility against the two previous versions on releases), and
-  you may have to prepare overlays for projects using the
-  compatibility flags.
-
-## About one month before the beta ##
-
-- [ ] Create the `X.X.0` milestone and set its due date.
-- [ ] Send an announcement of the upcoming freeze on Coqdev and ask people to
-  remove from the beta milestone what they already know won't be ready on time
-  (possibly postponing to the `X.X.0` milestone for minor bug fixes,
-  infrastructure and documentation updates).
-- [ ] Determine which issues should / must be fixed before the beta, add them
-  to the beta milestone, possibly with a
-  ["priority: blocker"](https://github.com/coq/coq/labels/priority%3A%20blocker)
-  label. Make sure that all these issues are assigned (and that the assignee
-  provides an ETA).
-- [ ] Ping the development coordinator (**@mattam82**) to get him started on
-  the update to the Credits chapter of the reference manual.
-  See also [#7058](https://github.com/coq/coq/issues/7058).
-
-  The command that was used in the previous versions to get the list
-  of contributors for this version is `git shortlog -s -n
-  VX.X+alpha..master | cut -f2 | sort -k 2`. Note that the ordering is
-  approximative as it will misplace people with middle names. It is
-  also probably not correctly handling `Co-authored-by` info that we
-  have been using more lately, so should probably be updated to
-  account for this.
-
-## On the date of the feature freeze ##
-
-- [ ] Create the new version branch `vX.X` (using this name will ensure that
-  the branch will be automatically protected).
-- [ ] 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). You can use the `dev/tools/pin-ci.sh` script to do this
-  semi-automatically.
-  - [ ] Notify upstream authors about the pinning, see
-    `dev/tools/notify-upstream-pins.sh`. As of today there is no automated
-    way to track these issues.
-- [ ] Remove all remaining unmerged feature PRs from the beta milestone.
+  Therefore, if you proceeded as described above, this should be the
+  commit updating the version, magic numbers and compatibility
+  infrastructure.  After tagging, double-check that `git describe`
+  picks up the tag you just made (if not, you tagged the wrong
+  commit).
+- [ ] Push the new tag with `git push upstream VY.Y+alpha --dry-run`
+  (remove the `--dry-run` and redo if everything looks OK).
 - [ ] Start a new project to track PR backporting. The project should
-  have a "Request X.X+beta1 inclusion" column for the PRs that were
+  have a `Request X.X+rc1 inclusion` column for the PRs that were
   merged in `master` that are to be considered for backporting, and a
-  "Shipped in X.X+beta1" columns to put what was backported. A message
-  to **@coqbot** in the milestone description tells it to
-  automatically add merged PRs to the "Request ... inclusion" column
-  and backported PRs to the "Shipped in ..." column. See previous
-  milestones for examples. When moving to the next milestone
-  (e.g. X.X.0), you can clear and remove the "Request X.X+beta1
-  inclusion" column and create new "Request X.X.0 inclusion" and
-  "Shipped in X.X.0" columns.
+  `Shipped in X.X+rc1` columns to put what was backported. A message
+  to `@coqbot` in the milestone description tells it to automatically
+  add merged PRs to the `Request ... inclusion` column and backported
+  PRs to the `Shipped in ...` column. See previous milestones for
+  examples. When moving to the next milestone (e.g. `X.X.0`), you can
+  clear and remove the `Request X.X+rc1 inclusion` column and create
+  new `Request X.X.0 inclusion` and `Shipped in X.X.0` columns.
 
   The release manager is the person responsible for merging PRs that
-  target the version branch and backporting appropriate PRs that are
-  merged into `master`.
-- [ ] Delay non-blocking issues to the appropriate milestone and ensure
-  blocking issues are solved. If required to solve some blocking issues,
-  it is possible to revert some feature PRs in the version branch only.
-- [ ] Add a new link to the ``'versions'`` list of the refman (in
-      ``html_context`` in ``doc/sphinx/conf.py``).
-
-## Before the beta release date ##
-
-- [ ] Ensure the Credits chapter has been updated.
-- [ ] Prepare the release notes (see e.g.,
-  [#10833](https://github.com/coq/coq/pull/10833)): in a PR against the `master`
-  branch, move the contents from all files of `doc/changelog/` that appear in
-  the release branch into the manual `doc/sphinx/changes.rst`. Merge that PR
-  into the `master` branch and backport it to the version branch.
-- [ ] Ensure that an appropriate version of the plugins we will distribute with
-  Coq has been tagged.
-- [ ] Have some people test the recently auto-generated Windows and MacOS
-  packages.
+  target the release branch and backporting appropriate PRs (mostly
+  safe bug fixes, user message improvements and documentation updates)
+  that are merged into `master`.
+- [ ] Pin the versions of libraries and plugins in
+  [`dev/ci/ci-basic-overlay.sh`](../ci/ci-basic-overlay.sh) to use
+  commit hashes. You can use the
+  [`dev/tools/pin-ci.sh`](../tools/pin-ci.sh) script to do this
+  semi-automatically.
+- [ ] In a PR on `master` to be backported, add a new link to the
+  `'versions'` list of the refman (in `html_context` in
+  [`doc/sphinx/conf.py`](../../doc/sphinx/conf.py)).
+
+## In the days following the branching ##
+
+- [ ] Make sure that all the last feature PRs that you want to include
+  in the release are finished and backported quickly and clean up the
+  milestone.  We recommend backporting as few feature PRs as possible
+  after branching.  In particular, any PR with overlays will require
+  manually bumping the pinned commits when backporting.
+- [ ] Delay non-blocking issues to the appropriate milestone and
+  ensure blocking issues are solved. If required to solve some
+  blocking issues, it is possible to revert some feature PRs in the
+  release branch only (but in this case, the blocking issue should be
+  postponed to the next major release instead of being closed).
+- [ ] Once the final list of features is known, in a PR on `master` to
+  be backported, generate the release changelog by calling
+  [`dev/tools/generate-release-changelog.sh`](../tools/generate-release-changelog.sh)
+  and include it in a new section in
+  [`doc/sphinx/changes.rst`](../../doc/sphinx/changes.rst).
+
+  At the moment, the script doesn't do it automatically, but we
+  recommend reordering the entries to show first the **Changed**, then
+  the **Removed**, **Deprecated**, **Added** and last the **Fixed**.
+- [ ] Ping the development coordinator (`@mattam82`) to get him
+  started on writing the release summary.
+
+  The `dev/tools/list-contributors.sh` script computes the number and
+  list of contributors between Coq revisions. Typically used with
+  `VX.X+alpha..vX.X` to check the contributors of version `VX.X`.
+
+## For each release (preview, final, patch-level) ##
+
+- [ ] Ensure that there exists a milestone for the following version.
+- [ ] Ensure the release changelog has been merged (the release
+  summary is required for the final release).
 - [ ] In a PR against `vX.X` (for testing):
-  - Change the version name from alpha to beta1 (see
-  [#7009](https://github.com/coq/coq/pull/7009/files)).
-  - We generally do not update the magic numbers at this point.
+  - Update the version number.
+  - Only update the magic numbers for the final release (see
+    [#7271](https://github.com/coq/coq/pull/7271/files)).
   - Set `is_a_released_version` to `true` in `configure.ml`.
-- [ ] Put the `VX.X+beta1` tag using `git tag -s`.
-- [ ] Push the new tag with `git push upstream VX.X+beta1 --dry-run`
-  (remove the `--dry-run` and redo if all looks OK).
-- [ ] Set `is_a_released_version` to `false` in `configure.ml`
-  (if you forget about it, you'll be reminded whenever you try to
-  backport a PR with a changelog entry).
-
-### These steps are the same for all releases (beta, final, patch-level) ###
-
-- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that
-  package managers can start preparing package updates (including a
-  `coq-bignums` compatible version).
-- [ ] When opening the corresponding PR for `coq` in the opam repository ([`coq/opam-coq-archive`](https://github.com/coq/opam-coq-archive) or [`ocaml/opam-repository`](https://github.com/ocaml/opam-repository)),
-  the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq)
-  (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built).
-- [ ] Draft a release on GitHub.
-- [ ] Sign the Windows and MacOS packages and upload them on GitHub.
-  + The Windows packages must be signed by the Inria IT security service. They
-    should be sent as a link to the binary (via [filesender](https://filesender.renater.fr) for example)
-    together with its SHA256 hash in a signed e-mail to `dsi.securite` @ `inria.fr`
-    putting `@maximedenes` in carbon copy.
-  + The MacOS packages should be signed with our own certificate. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases).
-- [ ] Prepare a page of news on the website with the link to the GitHub release
-  (see [coq/www#63](https://github.com/coq/www/pull/63)).
-- [ ] Merge the website update, publish the release
-  and send announcement e-mails, typically on
-  the `coq-club@inria.fr` mailing list and the discourse forum
-    ([posting by mail](https://github.com/coq/coq/wiki/Discourse))
+- [ ] Set the tag `VX.X...` using `git tag -s`.
+- [ ] Push the new tag with `git push upstream VX.X... --dry-run`
+  (remove the `--dry-run` and redo if everything looks OK).
+- [ ] Set `is_a_released_version` to `false` in `configure.ml` (if you
+  forget about it, you'll be reminded by the test-suite failing
+  whenever you try to backport a PR with a changelog entry).
 - [ ] Close the milestone
-
-## At the final release time ##
-
-- [ ] Prepare the release notes (see above)
-- [ ] In a PR against `vX.X` (for testing):
-  - Change the version name from X.X.0 and the magic numbers (see
-  [#7271](https://github.com/coq/coq/pull/7271/files)).
-  - Set `is_a_released_version` to `true` in `configure.ml`.
-- [ ] Put the `VX.X.0` tag.
-- [ ] Push the new tag with `git push upstream VX.X.0 --dry-run`
-  (remove the `--dry-run` and redo if all looks OK).
-- [ ] Set `is_a_released_version` to `false` in `configure.ml`
-  (if you forget about it, you'll be reminded whenever you try to
-  backport a PR with a changelog entry).
-
-Repeat the generic process documented above for all releases.
-
-Ping `@Zimmi48` to:
-
-- [ ] Switch the default version of the reference manual on the website.
+- [ ] Send an e-mail on Coqdev + the Coq development category on
+  Discourse (coqdev@inria.fr + coq+coq-development@discoursemail.com)
+  announcing that the tag has been set so that package managers can
+  start preparing package updates (including a `coq-bignums`
+  compatible version).
+- [ ] In particular, ensure that someone is working on providing an
+  opam package (either in the main
+  [ocaml/opam-repository](https://github.com/ocaml/opam-repository)
+  for standard releases or in the `core-dev` category of the
+  [coq/opam-coq-archive](https://github.com/coq/opam-coq-archive)
+  for preview releases.
+- [ ] Make sure to cc `@erikmd` to request that he prepare the
+  necessary configuration for the Docker release in
+  [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq) (namely, he'll
+  need to make sure a `coq-bignums` opam package is available in
+  [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev),
+  respectively
+  [`released`](https://github.com/coq/opam-coq-archive/tree/master/released),
+  so the Docker image gathering `coq` and `coq-bignums` can be built).
+- [ ] Publish a release on GitHub with the PDF version of the
+  reference manual attached.
+
+## For each non-preview release ##
+
+- [ ] Ping `@Zimmi48` to switch the default version of the reference
+  manual on the website.
 
   This is done by logging into the server (`vps697916.ovh.net`),
   editing two `ProxyPass` lines (one for the refman and one for the
@@ -181,11 +167,30 @@ Ping `@Zimmi48` to:
   repository. See [coq/www#111](https://github.com/coq/www/issues/111)
   and [coq/www#131](https://github.com/coq/www/issues/131).
 
-- [ ] Publish a new version on Zenodo (only once per major version).
+## Only for the final release of each major version ##
+
+- [ ] Ping `@Zimmi48` to publish a new version on Zenodo.
 
   *TODO:* automate this with coqbot.
 
-## At the patch-level release time ##
+## This is now delegated to the platform maintainers ##
 
-We generally do not update the magic numbers at this point (see
-[`2881a18`](https://github.com/coq/coq/commit/2881a18)).
+- [ ] Sign the Windows and MacOS packages and upload them on GitHub.
+  + The Windows packages must be signed by the Inria IT security
+    service. They should be sent as a link to the binary (via
+    [filesender](https://filesender.renater.fr) for example) together
+    with its SHA256 hash in a signed e-mail to `dsi.securite` @
+    `inria.fr` putting `@maximedenes` in carbon copy.
+  + The MacOS packages should be signed with our own certificate. A
+    detailed step-by-step guide can be found [on the
+    wiki](https://github.com/coq/coq/wiki/SigningReleases).
+  + The Snap package has to be built and uploaded to the snap store by
+    running a [platform CI job
+    manually](https://github.com/coq/platform/tree/v8.13/linux/snap/github_actions).
+    Then ask `@gares` to publish the upload or give you the password
+    for the `coq-team` account on the store so that you can do it
+    yourself.
+- [ ] Prepare a PR on [coq/www](https://github.com/coq/www) adding a
+  page of news on the website.
+- [ ] Announce the release to Coq-Club and Discourse
+  (coq-club@inria.fr + coq+announcements@discoursemail.com).
diff --git a/dev/dune b/dev/dune
index a6d88c94d2..9da06a3fab 100644
--- a/dev/dune
+++ b/dev/dune
@@ -1,11 +1,11 @@
 (library
  (name top_printers)
- (public_name coq.top_printers)
+ (public_name coq-core.top_printers)
  (synopsis "Coq's Debug Printers")
  (wrapped false)
  (modules top_printers)
  (optional)
- (libraries coq.toplevel coq.plugins.ltac))
+ (libraries coq-core.toplevel coq-core.plugins.ltac))
 
 (rule
   (targets dune-dbg)
@@ -17,26 +17,27 @@
     ; We require all the OCaml libs to be in place and searchable
     ; by OCamlfind, this is a bit of a hack but until Dune gets
     ; proper ocamldebug support we have to live with that.
-    %{lib:coq.config:config.cma}
-    %{lib:coq.clib:clib.cma}
-    %{lib:coq.lib:lib.cma}
-    %{lib:coq.kernel:kernel.cma}
-    %{lib:coq.vm:byterun.cma}
-    %{lib:coq.vm:../../stublibs/dllbyterun_stubs.so}
-    %{lib:coq.library:library.cma}
-    %{lib:coq.engine:engine.cma}
-    %{lib:coq.pretyping:pretyping.cma}
-    %{lib:coq.gramlib:gramlib.cma}
-    %{lib:coq.interp:interp.cma}
-    %{lib:coq.proofs:proofs.cma}
-    %{lib:coq.parsing:parsing.cma}
-    %{lib:coq.printing:printing.cma}
-    %{lib:coq.tactics:tactics.cma}
-    %{lib:coq.vernac:vernac.cma}
-    %{lib:coq.stm:stm.cma}
-    %{lib:coq.toplevel:toplevel.cma}
-    %{lib:coq.plugins.ltac:ltac_plugin.cma}
-    %{lib:coq.top_printers:top_printers.cmi}
-    %{lib:coq.top_printers:top_printers.cma}
-    %{lib:coq.top_printers:../META})
+    %{lib:coq-core.config:config.cma}
+    %{lib:coq-core.clib:clib.cma}
+    %{lib:coq-core.lib:lib.cma}
+    %{lib:coq-core.kernel:kernel.cma}
+    %{lib:coq-core.vm:byterun.cma}
+    %{lib:coq-core.vm:../../stublibs/dllbyterun_stubs.so}
+    %{lib:coq-core.library:library.cma}
+    %{lib:coq-core.engine:engine.cma}
+    %{lib:coq-core.pretyping:pretyping.cma}
+    %{lib:coq-core.gramlib:gramlib.cma}
+    %{lib:coq-core.interp:interp.cma}
+    %{lib:coq-core.proofs:proofs.cma}
+    %{lib:coq-core.parsing:parsing.cma}
+    %{lib:coq-core.printing:printing.cma}
+    %{lib:coq-core.tactics:tactics.cma}
+    %{lib:coq-core.vernac:vernac.cma}
+    %{lib:coq-core.stm:stm.cma}
+    %{lib:coq-core.sysinit:sysinit.cma}
+    %{lib:coq-core.toplevel:toplevel.cma}
+    %{lib:coq-core.plugins.ltac:ltac_plugin.cma}
+    %{lib:coq-core.top_printers:top_printers.cmi}
+    %{lib:coq-core.top_printers:top_printers.cma}
+    %{lib:coq-core.top_printers:../META})
   (action (copy dune-dbg.in dune-dbg)))
diff --git a/dev/dune_db_408 b/dev/dune_db_408
index 5f826fe383..bc86020d56 100644
--- a/dev/dune_db_408
+++ b/dev/dune_db_408
@@ -17,6 +17,7 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
 
diff --git a/dev/dune_db_409 b/dev/dune_db_409
index 2e58272c75..adb1f76872 100644
--- a/dev/dune_db_409
+++ b/dev/dune_db_409
@@ -16,6 +16,7 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
 
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 534f20f85b..db15d9705a 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -19,7 +19,7 @@ exec $OCAMLDEBUG \
     -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
     -I $COQTOP/gramlib/.pack \
     -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-    -I $COQTOP/library -I $COQTOP/engine \
+    -I $COQTOP/library -I $COQTOP/engine -I $COQTOP/sysinit \
     -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
     -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
     -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
diff --git a/dev/shim/dune b/dev/shim/dune
index 8006c629ed..e4cc7699f0 100644
--- a/dev/shim/dune
+++ b/dev/shim/dune
@@ -26,7 +26,7 @@
  (targets coqbyte-prelude)
  (deps
   %{bin:coqtop.byte}
-  %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so}
+  %{lib:coq-core.kernel:../../stublibs/dllbyterun_stubs.so}
   %{project_root}/theories/Init/Prelude.vo)
  (action
   (with-stdout-to %{targets}
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 5f9f326750..d4f599484f 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -33,7 +33,7 @@
 
 (defun coqdev-default-directory ()
   "Return the Coq repository containing `default-directory'."
-  (let ((dir (locate-dominating-file default-directory "META.coq.in")))
+  (let ((dir (locate-dominating-file default-directory "META.coq-core.in")))
     (when dir (expand-file-name dir))))
 
 (defun coqdev-setup-compile-command ()
diff --git a/dev/tools/list-contributors.sh b/dev/tools/list-contributors.sh
new file mode 100644
index 0000000000..c968f2e952
--- /dev/null
+++ b/dev/tools/list-contributors.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+# For compat with OSX which has a non-gnu sed which doesn't support -z
+SED=`which gsed || which sed`
+
+if [ $# != 1 ]; then
+  error "usage: $0 rev0..rev1"
+  exit 1
+fi
+
+git shortlog -s -n --group=author --group=trailer:Co-authored-by $1 | cut -f2 | sort -k 2 | grep -v -e "coqbot" -e "^$" > contributors.tmp
+
+cat contributors.tmp | wc -l | xargs echo "Contributors:"
+cat contributors.tmp | gsed -z "s/\n/, /g"
+echo
+rm contributors.tmp
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 666fb6cc91..a14b98c73c 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -64,7 +64,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2
 RELEASE_NUMBER_OF_OLD_VERSIONS = 2
 MASTER_NUMBER_OF_OLD_VERSIONS = 3
 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n'
-COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
+COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'sysinit', 'coqargs.ml')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
 TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f3d6239c6f..f8fd8b3d5b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -576,7 +576,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
+  let cmd_fn c ?loc:_ ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
   let cmd_class _ = VtQuery in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintConstr" [cmd]
@@ -585,7 +585,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
+  let cmd_fn c ?loc:_ ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
   let cmd_class _ = VtQuery in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintPureConstr" [cmd]
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index e8ed6c709e..b4b24d743a 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -165,6 +165,7 @@ val ppobj : Libobject.obj -> unit
 (* Some super raw printers *)
 val cast_kind_display : Constr.cast_kind -> string
 val constr_display : Constr.constr -> unit
+val econstr_display : EConstr.constr -> unit
 val print_pure_constr : Constr.types -> unit
 val print_pure_econstr : EConstr.types -> unit