11 files changed, 92 insertions, 7 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 7853866f62..4709247549 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -26,7 +26,8 @@ our CI. This means that:
 
 On the condition that:
 
-- At the time of the submission, your development works with Coq master branch.
+- At the time of the submission, your development works with Coq's
+  `master` branch.
 
 - Your development is publicly available in a git repository and we can easily
   send patches to you (e.g. through pull / merge requests).
@@ -60,6 +61,19 @@ performance benchmark. Currently this is done by providing an OPAM package
 in https://github.com/coq/opam-coq-archive and opening an issue at
 https://github.com/coq/coq-bench/issues.
 
+### Recommended branching policy.
+
+It is sometimes the case that you will need to maintain a branch of
+your development for particular Coq versions. This is in fact very
+likely if your development includes a Coq ML plugin.
+
+We thus recommend a branching convention that mirrors Coq's branching
+policy. Then, you would have a `master` branch that follows Coq's
+`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so
+on.
+
+This convention will be supported by tools in the future to make some
+developer commands work more seamlessly.
 
 Information for developers
 --------------------------
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index f422030b53..50d4d21637 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -238,7 +238,7 @@
 ########################################################################
 # plugin_tutorial
 ########################################################################
-: "${plugin_tutorial_CI_REF:=14b2976cdf67db788b79d9421ce1e89bd15c7313}"
+: "${plugin_tutorial_CI_REF:=master}"
 : "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
 : "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 41e1d1a937..4ddb582414 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-22-V1"
+# CACHEKEY: "bionic_coq-V2018-10-30-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,7 +37,7 @@ 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.2.1 ounit.2.0.8 odoc.1.3.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
@@ -53,10 +53,10 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM camlp5.$CAMLP5_VER
 
 # EDGE switch
-ENV COMPILER_EDGE="4.07.0" \
-    CAMLP5_VER_EDGE="7.06" \
+ENV COMPILER_EDGE="4.07.1" \
+    CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
-    BASE_OPAM_EDGE="dune-release.0.3.0"
+    BASE_OPAM_EDGE="dune-release.1.1.0"
 
 RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \
     opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh
new file mode 100755
index 0000000000..4605255d5e
--- /dev/null
+++ b/dev/ci/user-overlays/08515-command-atts.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then
+    ltac2_CI_REF=command-atts
+    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
+
+    Equations_CI_REF=command-atts
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    plugin_tutorial_CI_REF=command-atts
+    plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials
+fi
diff --git a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh
new file mode 100644
index 0000000000..9d723dc7f2
--- /dev/null
+++ b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh
@@ -0,0 +1,11 @@
+_OVERLAY_BRANCH=name-abstract-univ-context
+
+if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    Elpi_CI_REF="$_OVERLAY_BRANCH"
+    Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    Equations_CI_REF="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
new file mode 100644
index 0000000000..bd3e1bf7ff
--- /dev/null
+++ b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
@@ -0,0 +1,7 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then
+    plugin_tutorial_CI_REF=pr8671-fix
+    plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials
+
+fi
diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
new file mode 100644
index 0000000000..98530c825a
--- /dev/null
+++ b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then
+
+    Elpi_CI_REF=kernel-entries-cleanup
+    Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    Equations_CI_REF=kernel-entries-cleanup
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
new file mode 100644
index 0000000000..81ed91f52b
--- /dev/null
+++ b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then
+
+    Elpi_CI_REF=master+generalized-evar-printers-pr8688
+    Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh
new file mode 100644
index 0000000000..8ad8cba243
--- /dev/null
+++ b/dev/ci/user-overlays/08844-split-tactics.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then
+    Equations_CI_REF=split-tactics
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    ltac2_CI_REF=split-tactics
+    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
+
+    fiat_parsers_CI_REF=split-tactics
+    fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat
+fi
diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh
new file mode 100644
index 0000000000..17eb5fffae
--- /dev/null
+++ b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then
+
+    Equations_CI_REF=program-hook-obligation-subst
+    Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 68afe7ee4a..7fb73e447d 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -33,3 +33,11 @@ fi
 ```
 
 (`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh))
+
+### Branching conventions
+
+We suggest you use the convention of identical branch names for the
+Coq branch and the CI project branch used in the overlay. For example,
+if your Coq PR is coming from the branch `more_efficient_tc`, and that
+breaks `ltac2`, we suggest you create a `ltac2` overlay with a branch
+named `more_efficient_tc`.