Complete rewrite of the documentation of overlays after Jim's additional comments.

[ci skip]

2 files changed, 36 insertions, 24 deletions

diff --git a/dev/ci/README.md b/dev/ci/README.md
index ed3442e0db..697a160ca9 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -107,19 +107,32 @@ there are some.
 
 You can also run one CI target locally (using `make ci-somedev`).
 
-Whenever your PR breaks tested developments, you should either adapt it
-so that it doesn't, or provide a branch fixing these developments (or at
-least work with the author of the development / other Coq developers to
-prepare these fixes). Then, add an overlay in
-[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there)
-as part of your PR.
-
-The process to merge your PR is then to submit PRs to the external
-development repositories, merge the latter first (if the fixes are
-backward-compatible), and merge the PR on Coq then.
-
 See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
 
+### Breaking changes
+
+When your PR breaks an external project we test in our CI, you must prepare a
+patch (or ask someone to prepare a patch) to fix the project:
+
+1. Fork the external project, create a new branch, push a commit adapting
+   the project to your changes.
+2. Test your pull request with your adapted version of the external project by
+   adding an overlay file to your pull request (cf.
+   [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)).
+3. Fixes to external libraries (pure Coq projects) *must* be backward
+   compatible (i.e. they should also work with the development version of Coq,
+   and the latest stable version). This will allow you to open a PR on the
+   external project repository to have your changes merged *before* your PR on
+   Coq can be integrated.
+
+   On the other hand, patches to plugins (projects linking to the Coq ML API)
+   can very rarely be made backward compatible and plugins we test will
+   generally have a dedicated branch per Coq version.
+   You can still open a pull request but the merging will be requested by the
+   developer who merges the PR on Coq. There are plans to improve this, cf.
+   [#6724](https://github.com/coq/coq/issues/6724).
+
+Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file.
 
 Advanced GitLab CI information
 ------------------------------
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 8cbe8fc339..aec2dfe0a6 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,18 +1,17 @@
 # Add overlays for your pull requests in this directory
 
-When your pull request breaks an external development we test in our CI, you
-must prepare a patch (or ask someone to prepare a patch) to fix this development.
-Backward compatible patches are to be preferred, especially on libraries (it is
-harder to make backward compatible patches for plugins).
-
-Once you have a patched version, you can add an overlay to your pull request:
-this is a file which defines where to look for the patched version so that
-testing is possible. It changes the value of some variables from
-[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh) (generally both the
-`_CI_BRANCH` and the `_CI_GITURL` variables of a given development at once).
-
-The file contains very simple logic to test the pull request number or branch
-name and apply it only in this case.
+When your pull request breaks an external project we test in our CI and you
+have prepared a branch with the fix, you can add an "overlay" to your pull
+request to test it with the adapted version of the external project.
+
+An overlay is a file which defines where to look for the patched version so that
+testing is possible. It redefines some variables from
+[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh):
+give the name of your branch using a `_CI_BRANCH` variable and the location of
+your fork using a `_CI_GITURL` variable.
+
+Moreover, the file contains very simple logic to test the pull request number
+or branch name and apply it only in this case.
 
 The name of your overlay file should start with a five-digit pull request
 number, followed by a dash, anything (for instance your GitHub nickname