4 files changed, 42 insertions, 14 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 24952eb5b7..7853866f62 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project:
    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.
+Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
 
 Advanced GitLab CI information
 ------------------------------
@@ -175,6 +175,11 @@ If your repository has access to runners tagged `windows`, setting the
 secret variable `WINDOWS` to `enabled` will add jobs building Windows
 versions of Coq (32bit and 64bit).
 
+If the secret variable `WINDOWS` is set to `enabled_all_addons`,
+an extended set of addons will be added to the Windows installer.
+This leads to a considerable runtime in CI so this is not enabled
+by default for pipelines for pull requests.
+
 The Windows jobs are enabled on Coq's repository, where pipelines for
 pull requests run.
 
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index deda42e2b7..918d289ae2 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -37,8 +37,21 @@ SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
 SET COQREGTESTING=Y
 SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
 
-if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
-if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+IF "%WINDOWS%" == "enabled_all_addons" (
+  SET EXTRA_ADDONS=^
+    -addon=mathcomp ^
+    -addon=menhir ^
+    -addon=menhirlib ^
+    -addon=compcert ^
+    -addon=extlib ^
+    -addon=quickchick ^
+    -addon=coquelicot
+  REM addons with build issues
+  REM -addon=vst ^
+  REM -addon=aactactics ^
+) ELSE (
+  SET "EXTRA_ADDONS= "
+)
 
 call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
   -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
@@ -47,20 +60,10 @@ call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
   -addon=equations ^
   -addon=ltac2 ^
   -addon=mtac2 ^
-  -addon=mathcomp ^
-  -addon=menhir ^
-  -addon=menhirlib ^
-  -addon=compcert ^
-  -addon=extlib ^
-  -addon=quickchick ^
-  -addon=coquelicot ^
+  %EXTRA_ADDONS% ^
   -make=N ^
   -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
 
-REM addons with build issues
-REM -addon=vst ^
-REM -addon=aactactics ^
-
 ECHO "Start Artifact Creation"
 TIME /T
 
diff --git a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
new file mode 100644
index 0000000000..484ad8f9e6
--- /dev/null
+++ b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
@@ -0,0 +1,11 @@
+if [ "$CI_PULL_REQUEST" = "8554" ] || [ "$CI_BRANCH" = "master+fix8553-change-under-binders" ]; then
+
+    ltac2_CI_BRANCH=master+fix-pr8554-change-takes-env
+    ltac2_CI_REF=master+fix-pr8554-change-takes-env
+    ltac2_CI_GITURL=https://github.com/herbelin/ltac2
+
+    Equations_CI_BRANCH=master+fix-pr8554-change-takes-env
+    Equations_CI_REF=master+fix-pr8554-change-takes-env
+    Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
new file mode 100644
index 0000000000..41c2ad6fef
--- /dev/null
+++ b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then
+
+    ltac2_CI_REF=rm-section-path
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    Equations_CI_REF=rm-section-path
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi