6 files changed, 60 insertions, 23 deletions
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 03ce5a6b5d..ee6c62673b 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -2,7 +2,7 @@
 
 set -e -x
 
-OPAM_VARIANT=ocaml-variants.4.08.1+mingw64c
+OPAM_VARIANT=ocaml-variants.4.09.0+mingw64c
 
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
 tar -xf opam64.tar.xz
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 567f0539ab..edca83c6ef 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-07-09-V01"
+# CACHEKEY: "bionic_coq-V2019-09-20-V01"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,12 +37,12 @@ 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.10.0 ounit.2.0.8 odoc.1.4.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.7.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
+ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6"
 
 # Must add this to COQIDE_OPAM{,_EDGE} when we update the opam
 # packages "lablgtk3-gtksourceview3"
@@ -56,9 +56,9 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.08.1" \
-    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \
-    BASE_OPAM_EDGE="dune-release.1.3.1"
+ENV COMPILER_EDGE="4.09.0" \
+    COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \
+    BASE_OPAM_EDGE="dune-release.1.3.2"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh
new file mode 100644
index 0000000000..a5f6551474
--- /dev/null
+++ b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then
+
+    elpi_CI_REF=library+to_vernac_step2
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index d00c8cb11a..78d7061259 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -129,6 +129,18 @@ Universes
   GH issue number: #9294
   risk: moderate risk to be activated by chance
 
+  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 development branches: none
+  impacted coqchk versions: immune
+  fixed in: PR#10664
+  found by: Pédrot
+  exploit: no test
+  GH issue number: none
+  risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
+
 Primitive projections
 
   component: primitive projections, guard condition
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 452160ea5a..ea268f9d4e 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -2,6 +2,11 @@
 
 ## 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.
 - [ ] Change the version name to the next major version and the magic
@@ -54,25 +59,39 @@
 - [ ] 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 to get the list of contributors for this version is
-  `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2`
-  (the ordering is approximative as it will misplace people with middle names).
+
+  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).
 - [ ] Remove all remaining unmerged feature PRs from the beta milestone.
-- [ ] Start a new project to track PR backporting. The proposed model is to
-  have a "X.X-only PRs" column for the rare PRs on the stable branch, a
-  "Request X.X inclusion" column for the PRs that were merged in `master` that
-  are to be considered for backporting, a "Waiting for CI" column to put the
-  PRs in the process of being backported, and "Shipped in ..." columns to put
-  what was backported. (The release manager is the person responsible for
-  merging PRs that target the version branch and backporting appropriate PRs
-  that are merged into `master`).
-  A message to **@coqbot** in the milestone description tells it to
-  automatically add merged PRs to the "Request X.X inclusion" column.
+- [ ] Start a new project to track PR backporting. The project should
+  have a "Request X.X+beta1 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.
+
+  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.
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 7e53f13e45..28e8773e25 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -1,7 +1,7 @@
-(lang dune 1.4)
+(lang dune 1.10)
 
 ; Add custom flags here. Default developer profile is `dev`
 (context (opam (switch 4.05.0)))
 (context (opam (switch 4.05.0+32bit)))
-(context (opam (switch 4.08.1)))
-(context (opam (switch 4.08.1+flambda)))
+(context (opam (switch 4.09.0)))
+(context (opam (switch 4.09.0+flambda)))