4 files changed, 34 insertions, 9 deletions
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 918d289ae2..386a3de204 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -39,6 +39,10 @@ SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\
 
 IF "%WINDOWS%" == "enabled_all_addons" (
   SET EXTRA_ADDONS=^
+    -addon=bignums ^
+    -addon=equations ^
+    -addon=ltac2 ^
+    -addon=mtac2 ^
     -addon=mathcomp ^
     -addon=menhir ^
     -addon=menhirlib ^
@@ -56,10 +60,6 @@ IF "%WINDOWS%" == "enabled_all_addons" (
 call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
   -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
   -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-  -addon=bignums ^
-  -addon=equations ^
-  -addon=ltac2 ^
-  -addon=mtac2 ^
   %EXTRA_ADDONS% ^
   -make=N ^
   -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md
new file mode 100644
index 0000000000..1685b084e9
--- /dev/null
+++ b/dev/ci/nix/README.md
@@ -0,0 +1,19 @@
+# Working on third-party developments with *this* version of Coq
+
+Aim: getting an environment suitable for working on a third-party development
+using the current version of Coq (i.e., built from the current state of this
+repository).
+
+Dive into such an environment, for the project `example` by running, from the
+root of this repository:
+
+    ./dev/ci/nix/shell example
+
+This will build Coq and the other dependencies of the `example` project, then
+open a shell with all these dependencies available (e.g., `coqtop` is in path).
+
+Additionally, three environment variables are set, to abstract over the
+build-system of that project: `configure`, `make`, and `clean`. Therefore, after
+changing the working directory to the root of the sources of that project, the
+contents of these variables can be evaluated to respectively set-up, build, and
+clean the project.
diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq.nix
index f10afd5680..093c262cde 100644
--- a/dev/ci/nix/unicoq.nix
+++ b/dev/ci/nix/unicoq.nix
@@ -1,11 +1,8 @@
-{ stdenv, fetchzip, coq }:
+{ stdenv, coq }:
 
 stdenv.mkDerivation {
   name = "coq${coq.coq-version}-unicoq-0.0-git";
-  src = fetchzip {
-    url = "https://github.com/vbgl/unicoq/archive/8b33e37700e92bfd404bf8bf9fe03f1be8928d97.tar.gz";
-    sha256 = "0s4z0wjxlp56ccgzxgk04z7skw90rdnz39v730ffkgrjl38rr9il";
-  };
+  src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz;
 
   buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
 
diff --git a/dev/ci/user-overlays/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh
new file mode 100644
index 0000000000..482792d7cd
--- /dev/null
+++ b/dev/ci/user-overlays/08850-poly-local-univs.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8850" ] || [ "$CI_BRANCH" = "poly-local-univs" ]; then
+    formal_topology_CI_REF=poly-local-univs
+    formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology
+
+    paramcoq_CI_REF=poly-local-univs
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+fi