7 files changed, 60 insertions, 5 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6a740b9033..88d08a1724 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -72,10 +72,10 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil
 ### Experimental automatic overlay creation and building
 
 If you break external projects that are hosted on GitHub, you can use
-the `create-overlays.sh` script to automatically perform most of the
+the `create_overlays.sh` script to automatically perform most of the
 above steps. In order to do so, call the script as:
 ```
-./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac
+./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac
 ```
 replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR
 number. The script will:
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index c18e556da8..f7a8851af7 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -95,6 +95,13 @@
 : "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}"
 
 ########################################################################
+# coq-tools
+########################################################################
+: "${coq_tools_CI_REF:=master}"
+: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}"
+: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}"
+
+########################################################################
 # Coquelicot
 ########################################################################
 : "${coquelicot_CI_REF:=master}"
@@ -242,7 +249,7 @@
 # ext-lib
 ########################################################################
 : "${ext_lib_CI_REF:=master}"
-: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}"
+: "${ext_lib_CI_GITURL:=https://github.com/coq-community/coq-ext-lib}"
 : "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}"
 
 ########################################################################
diff --git a/dev/ci/ci-coq-tools.sh b/dev/ci/ci-coq-tools.sh
new file mode 100755
index 0000000000..9c95c49c9f
--- /dev/null
+++ b/dev/ci/ci-coq-tools.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coq_tools
+
+( cd "${CI_BUILD_DIR}/coq_tools" && make check || \
+  { RV=$?; echo "The build broke, if an overlay is needed, mention @JasonGross in describing the expected change in Coq that needs to be taken into account, and he'll prepare a fix for coq-tools"; exit $RV; } )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index e9f8324f28..7a9531216e 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download Flocq
 
-( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index c8ea59f08a..b3ced999f6 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -22,7 +22,7 @@ let ssreflect = coqPackages.ssreflect.overrideAttrs (o: {
   }); in
 
 let coq-ext-lib = coqPackages.coq-ext-lib.overrideAttrs (o: {
-    src = fetchTarball "https://github.com/coq-ext-lib/coq-ext-lib/tarball/master";
+    src = fetchTarball "https://github.com/coq-community/coq-ext-lib/tarball/master";
   }); in
 
 let simple-io =
diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
new file mode 100644
index 0000000000..cd6b408813
--- /dev/null
+++ b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
@@ -0,0 +1,24 @@
+if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then
+
+    coqhammer_CI_REF="evar-inst-list"
+    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
+
+    elpi_CI_REF="evar-inst-list"
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    equations_CI_REF="evar-inst-list"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    metacoq_CI_REF="evar-inst-list"
+    metacoq_CI_GITURL=https://github.com/ppedrot/metacoq
+
+    mtac2_CI_REF="evar-inst-list"
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+    quickchick_CI_REF="evar-inst-list"
+    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+    unicoq_CI_REF="evar-inst-list"
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
new file mode 100644
index 0000000000..6bee3c7bb6
--- /dev/null
+++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then
+
+    fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto
+
+    mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+    metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    metacoq_CI_GITURL=https://github.com/herbelin/template-coq
+
+    unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    unimath_CI_GITURL=https://github.com/herbelin/UniMath
+
+fi