4 files changed, 61 insertions, 14 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index ed3442e0d..697a160ca 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/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index feabf72d4..48a1366ab 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -11,4 +11,4 @@ git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypt
 
 fiat_crypto_CI_TARGETS1="printlite lite lite-display"
 fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
-( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make ${fiat_crypto_CI_TARGETS2} )
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
new file mode 100644
index 000000000..ea9cd8ee0
--- /dev/null
+++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then
+
+    # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550
+    #
+    # equations
+    # ltac2
+
+    # The below developments should instead use a backwards compatible fix.
+    #
+    # color
+    # iris-lambda-rust
+    # math-classes
+    # formal-topology
+
+    ltac2_CI_BRANCH=tactics+push_fix_naming_out
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Equations_CI_BRANCH=tactics+push_fix_naming_out
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index a7474e324..aec2dfe0a 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,8 +1,21 @@
 # Add overlays for your pull requests in this directory
 
-An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+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.
 
-The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+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
+and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
 
 Example: `00669-maximedenes-ssr-merge.sh` containing