15 files changed, 125 insertions, 29 deletions
diff --git a/dev/build/windows/patches_coq/ocaml-4.07.1.patch b/dev/build/windows/patches_coq/ocaml-4.07.1.patch
index 2d61b5b838..2d61b5b838 100755..100644
--- a/dev/build/windows/patches_coq/ocaml-4.07.1.patch
+++ b/dev/build/windows/patches_coq/ocaml-4.07.1.patch
diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c
index c4c7ec2bff..c4c7ec2bff 100755..100644
--- a/dev/build/windows/patches_coq/pkg-config.c
+++ b/dev/build/windows/patches_coq/pkg-config.c
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/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 3923fea30e..8db0087e3c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -311,3 +311,10 @@
 : "${argosy_CI_REF:=master}"
 : "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}"
 : "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}"
+
+########################################################################
+# perennial
+########################################################################
+: "${perennial_CI_REF:=master}"
+: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
+: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh
new file mode 100755
index 0000000000..f3be66e814
--- /dev/null
+++ b/dev/ci/ci-perennial.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+FORCE_GIT=1
+git_download perennial
+
+# required by Perennial's coqc.py build wrapper
+export LC_ALL=C.UTF-8
+
+( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false )
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/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh
new file mode 100644
index 0000000000..d7af6b7a36
--- /dev/null
+++ b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10811" ] || [ "$CI_BRANCH" = "sprop-default-on" ]; then
+
+    elpi_CI_REF=sprop-default-on
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    coq_dpdgraph_CI_REF=sprop-default-on
+    coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph
+
+fi
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index a14781a058..b8987b7086 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -89,7 +89,7 @@ enables partial recalculation of dependencies (only the dependencies
 of changed files are recomputed).
 
 If you add a dependency to a Coq camlp5 extension (grammar.cma or
-q_constr.cmo), then see sections ".ml4 files" and "new files".
+q_constr.cmo), then see sections ".mlg files" and "new files".
 
 Cleaning Targets
 ----------------
@@ -113,13 +113,13 @@ Targets for cleaning various parts:
 
  - docclean: clean documentation
 
-.ml4/.mlp files
+.mlg/.mlp files
 ---------------
 
 There is now two kinds of preprocessed files : 
  - a .mlp do not need grammar.cma (they are in grammar/)
- - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
-   except coqide_main.ml4 and its specific rule
+ - a .mlg is now always preprocessed with grammar.cma (and q_constr.cmo),
+   except coqide_main.mlg and its specific rule
 
 This classification replaces the old mechanism of declaring the use
 of a grammar extension via a line of the form:
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index e5e4f740bd..096ffe6a1c 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -20,7 +20,7 @@ Special components
 grammar :
 
  Camlp5 syntax extensions. The file grammar/grammar.cma is used
- to pre-process .ml4 files containing EXTEND constructions,
+ to pre-process .mlg files containing EXTEND constructions,
  either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND.
  This grammar.cma incorporates many files from other directories
  (mainly parsing/), plus some specific files in grammar/.
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..1c486b024d 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.
@@ -80,6 +99,11 @@
 ## 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
@@ -120,6 +144,7 @@
 
 ## At the final release time ##
 
+- [ ] Prepare the release notes (see above)
 - [ ] In a PR:
   - Change the version name from X.X.0 and the magic numbers (see
   [#7271](https://github.com/coq/coq/pull/7271/files)).
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)))
diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
new file mode 100755
index 0000000000..ea96de970a
--- /dev/null
+++ b/dev/tools/make-changelog.sh
@@ -0,0 +1,25 @@
+#!/bin/sh
+
+echo "PR number"
+read -r PR
+
+echo "Where? (type a prefix)"
+(cd doc/changelog && ls -d */)
+read -r where
+
+where=$(echo doc/changelog/"$where"*)
+where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst"
+
+# shellcheck disable=SC2016
+# the ` are regular strings, this is intended
+# use %s for the leading - to avoid looking like an option (not sure
+# if necessary but doesn't hurt)
+printf '%s bla bla (`#%s <https://github.com/coq/coq/pull/%s>`_, by %s).' - "$PR" "$PR" "$(git config user.name)" > "$where"
+
+giteditor=$(git config core.editor)
+if [ "$giteditor" ]; then
+    $giteditor "$where"
+elif [ "$EDITOR" ]; then
+    $EDITOR "$where"
+else echo "$where"
+fi
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 601d52ddda..2f5c7128e2 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -727,7 +727,7 @@ Conflicts exists between integers and constrs.
 \nlsep \TERM{setoid_replace} ~\tacconstr ~\KWD{with} ~\tacconstr
 \nlsep \TERM{setoid_rewrite} ~\NT{orient} ~\tacconstr
 \nlsep \TERM{subst} ~\STAR{\NT{ident}}
-%% eqdecide.ml4
+%% eqdecide.mlg
 \nlsep \TERM{decide}~\TERM{equality} ~\OPTGR{\tacconstr~\tacconstr}
 \nlsep \TERM{compare}~\tacconstr~\tacconstr
 %% eauto