5 files changed, 53 insertions, 1 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/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/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/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`.