Merge PR #13177: Automatically merge overlays with most recent upstream version

Reviewed-by: Zimmi48

31 files changed, 58 insertions, 295 deletions

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f9187d53a6..d6f68fb0e9 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -44,6 +44,18 @@ CI_BUILD_DIR="$PWD/_build_ci"
 
 ls -l "$CI_BUILD_DIR" || true
 
+declare -A overlays
+
+overlay()
+{
+    local project=$1
+    local ov_url=$2
+    local ov_ref=$3
+
+    overlays[${project}_URL]=$ov_url
+    overlays[${project}_REF]=$ov_ref
+}
+
 set +x
 for overlay in "${ci_dir}"/user-overlays/*.sh; do
     # shellcheck source=/dev/null
@@ -62,32 +74,43 @@ set -x
 # (local build), it uses git clone to perform the download.
 git_download()
 {
-  local PROJECT=$1
-  local DEST="$CI_BUILD_DIR/$PROJECT"
-  local GITURL_VAR="${PROJECT}_CI_GITURL"
-  local GITURL="${!GITURL_VAR}"
-  local REF_VAR="${PROJECT}_CI_REF"
-  local REF="${!REF_VAR}"
-
-  if [ -d "$DEST" ]; then
-    echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists."
-  elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then
-    git clone "$GITURL" "$DEST"
-    cd "$DEST"
-    git checkout "$REF"
+  local project=$1
+  local dest="$CI_BUILD_DIR/$project"
+
+  local giturl_var="${project}_CI_GITURL"
+  local giturl="${!giturl_var}"
+  local ref_var="${project}_CI_REF"
+  local ref="${!ref_var}"
+
+  local ov_url=${overlays[${project}_URL]}
+  local ov_ref=${overlays[${project}_REF]}
+
+  if [ -d "$dest" ]; then
+    echo "Warning: download and unpacking of $project skipped because $dest already exists."
+  elif [[ $ov_url ]] || [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then
+    git clone "$giturl" "$dest"
+    cd "$dest"
+    git checkout "$ref"
+    git log -n 1
+    if [[ $ov_url ]]; then
+        git -c pull.rebase=false pull --no-ff "$ov_url" "$ov_ref"
+        git log -n 1 HEAD^2
+        git log -n 1
+    fi
   else # When possible, we download tarballs to reduce bandwidth and latency
-    local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL"
-    local ARCHIVEURL="${!ARCHIVEURL_VAR}"
-    mkdir -p "$DEST"
-    cd "$DEST"
-    local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1)
-    if [[ "$COMMIT" == "" ]]; then
-      # $REF must have been a tag or hash, not a branch
-      COMMIT="$REF"
+    local archiveurl_var="${project}_CI_ARCHIVEURL"
+    local archiveurl="${!archiveurl_var}"
+    mkdir -p "$dest"
+    cd "$dest"
+    local commit
+    commit=$(git ls-remote "$giturl" "refs/heads/$ref" | cut -f 1)
+    if [[ "$commit" == "" ]]; then
+      # $ref must have been a tag or hash, not a branch
+      commit="$ref"
     fi
-    wget "$ARCHIVEURL/$COMMIT.tar.gz"
-    tar xfz "$COMMIT.tar.gz" --strip-components=1
-    rm -f "$COMMIT.tar.gz"
+    wget "$archiveurl/$commit.tar.gz"
+    tar xfz "$commit.tar.gz" --strip-components=1
+    rm -f "$commit.tar.gz"
   fi
 }
 
diff --git a/dev/ci/user-overlays/08743-ejgallego-zarith.sh b/dev/ci/user-overlays/08743-ejgallego-zarith.sh
deleted file mode 100644
index da1d30c1e9..0000000000
--- a/dev/ci/user-overlays/08743-ejgallego-zarith.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11742" ] || [ "$CI_BRANCH" = "zarith+core" ]; then
-
-    bignums_CI_REF=zarith
-    bignums_CI_GITURL=https://github.com/ejgallego/bignums
-
-fi
diff --git a/dev/ci/user-overlays/10390-SkySkimmer-uip.sh b/dev/ci/user-overlays/10390-SkySkimmer-uip.sh
deleted file mode 100644
index 80107ac9c5..0000000000
--- a/dev/ci/user-overlays/10390-SkySkimmer-uip.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10390" ] || [ "$CI_BRANCH" = "uip" ]; then
-
-    unicoq_CI_REF=uip
-    unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq
-
-    mtac2_CI_REF=uip
-    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
-
-    elpi_CI_REF=uip
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-    equations_CI_REF=uip
-    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    paramcoq_CI_REF=uip
-    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
-
-    relation_algebra_CI_REF=uip
-    relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra
-
-    coq_dpdgraph_CI_REF=uip
-    coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph
-
-    coqhammer_CI_REF=uip
-    coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer
-
-    metacoq_CI_REF=uip
-    metacoq_CI_GITURL=https://github.com/SkySkimmer/metacoq
-
-fi
diff --git a/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh b/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh
deleted file mode 100644
index 05192facbe..0000000000
--- a/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11566" ] || [ "$CI_BRANCH" = "exninfo+coercion" ]; then
-
-    mtac2_CI_REF=exninfo+coercion
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/11604-persistent-arrays.sh b/dev/ci/user-overlays/11604-persistent-arrays.sh
deleted file mode 100644
index aec5c4fa3d..0000000000
--- a/dev/ci/user-overlays/11604-persistent-arrays.sh
+++ /dev/null
@@ -1,18 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11604" ] || [ "$CI_BRANCH" = "persistent-arrays" ]; then
-
-    unicoq_CI_REF=persistent-arrays
-    unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
-
-    elpi_CI_REF=persistent-arrays
-    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
-
-    #relation_algebra_CI_REF=persistent-arrays
-    #relation_algebra_CI_GITURL=https://github.com/maximedenes/relation-algebra
-
-    coqhammer_CI_REF=persistent-arrays
-    coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer
-
-    metacoq_CI_REF=persistent-arrays
-    metacoq_CI_GITURL=https://github.com/maximedenes/metacoq
-
-fi
diff --git a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
deleted file mode 100644
index 72ec55a37c..0000000000
--- a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
+++ /dev/null
@@ -1,18 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11836" ] || [ "$CI_BRANCH" = "obligations+functional" ]; then
-
-    mtac2_CI_REF=obligations+functional
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-    paramcoq_CI_REF=obligations+functional
-    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
-
-    equations_CI_REF=obligations+functional
-    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    metacoq_CI_REF=obligations+functional
-    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
-
-    rewriter_CI_REF=obligations+functional
-    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
-
-fi
diff --git a/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh
deleted file mode 100644
index c9ddb3fb9f..0000000000
--- a/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11922" ] || [ "$CI_BRANCH" = "rm-local-reductionops" ]; then
-
-    equations_CI_REF="rm-local-reductionops"
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-    unicoq_CI_REF="rm-local-reductionops"
-    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
-
-fi
diff --git a/dev/ci/user-overlays/11948-proux01-hexadecimal.sh b/dev/ci/user-overlays/11948-proux01-hexadecimal.sh
deleted file mode 100644
index 0b3133d1f1..0000000000
--- a/dev/ci/user-overlays/11948-proux01-hexadecimal.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11948" ] || [ "$CI_BRANCH" = "hexadecimal" ]; then
-
-    stdlib2_CI_REF=hexadecimal
-    stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
-
-    paramcoq_CI_REF=hexadecimal
-    paramcoq_CI_GITURL=https://github.com/proux01/paramcoq
-
-    metacoq_CI_REF=hexadecimal
-    metacoq_CI_GITURL=https://github.com/proux01/metacoq
-
-fi
diff --git a/dev/ci/user-overlays/12267-gares-elpi-1.11.sh b/dev/ci/user-overlays/12267-gares-elpi-1.11.sh
deleted file mode 100644
index ceb7afe3d1..0000000000
--- a/dev/ci/user-overlays/12267-gares-elpi-1.11.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12267" ] || [ "$CI_BRANCH" = "elpi-1.11" ]; then
-
-    elpi_CI_REF="coq-master+elpi-1.11"
-    elpi_hb_CI_REF="coq-master+elpi.11"
-
-fi
diff --git a/dev/ci/user-overlays/12372-ejgallego-proof+info.sh b/dev/ci/user-overlays/12372-ejgallego-proof+info.sh
deleted file mode 100644
index b9fdc338b5..0000000000
--- a/dev/ci/user-overlays/12372-ejgallego-proof+info.sh
+++ /dev/null
@@ -1,24 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12372" ] || [ "$CI_BRANCH" = "proof+info" ]; then
-
-    rewriter_CI_REF=proof+info
-    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
-
-    paramcoq_CI_REF=proof+info
-    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
-
-    mtac2_CI_REF=proof+info
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-    equations_CI_REF=proof+info
-    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    elpi_CI_REF=proof+info
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-    aac_tactics_CI_REF=proof+info
-    aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
-
-    metacoq_CI_REF=proof+info
-    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
-
-fi
diff --git a/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh
deleted file mode 100644
index ced0d95945..0000000000
--- a/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12505" ] || [ "$CI_BRANCH" = "factor-hint-flags" ]; then
-
-    fiat_parsers_CI_REF="factor-hint-flags"
-    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
-
-fi
diff --git a/dev/ci/user-overlays/12523-term-notation-custom.sh b/dev/ci/user-overlays/12523-term-notation-custom.sh
deleted file mode 100644
index 6217312a2a..0000000000
--- a/dev/ci/user-overlays/12523-term-notation-custom.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12523" ] || [ "$CI_BRANCH" = "fix-11121" ]; then
-
-    equations_CI_REF=fix-11121
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh b/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh
deleted file mode 100644
index 7c04608403..0000000000
--- a/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12565" ] || [ "$CI_BRANCH" = "fix-tc-search-opacity" ]; then
-
-    coqhammer_CI_REF=fix-tc-search-opacity
-    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
-
-fi
diff --git a/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh b/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh
deleted file mode 100644
index c8c5b3ed5a..0000000000
--- a/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12599" ] || [ "$CI_BRANCH" = "rm-deprecated-refiner" ]; then
-
-    equations_CI_REF=rm-deprecated-refiner
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh b/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh
deleted file mode 100644
index d4c67b03b5..0000000000
--- a/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12650" ] || [ "$CI_BRANCH" = "rebuild-record" ]; then
-
-    elpi_CI_REF=rebuild-record
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh
deleted file mode 100644
index 56a69abbf7..0000000000
--- a/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12709" ] || [ "$CI_BRANCH" = "hint-pattern-out" ]; then
-
-    coqhammer_CI_REF=hint-pattern-out
-    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
-
-fi
diff --git a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh
deleted file mode 100644
index e57f95ef19..0000000000
--- a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12720" ] || [ "$CI_BRANCH" = "factor-class-hint-clenv" ]; then
-
-    coqhammer_CI_REF=factor-class-hint-clenv
-    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
-
-fi
diff --git a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh
deleted file mode 100644
index 54fdd87566..0000000000
--- a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then
-
-    mathcomp_CI_REF=dont-refresh-argument-names-overlay
-    mathcomp_CI_GITURL=https://github.com/jashug/math-comp
-
-    oddorder_CI_REF=dont-refresh-argument-names-overlay
-    oddorder_CI_GITURL=https://github.com/jashug/odd-order
-
-fi
diff --git a/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh b/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh
deleted file mode 100644
index 6a9cf78687..0000000000
--- a/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12801" ] || [ "$CI_BRANCH" = "CyclicSet" ]; then
-
-    bignums_CI_REF=CyclicSet
-    bignums_CI_GITURL=https://github.com/VincentSe/bignums
-
-    coqprime_CI_REF=CyclicSet
-    coqprime_CI_GITURL=https://github.com/VincentSe/coqprime
-fi
diff --git a/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh
deleted file mode 100644
index bb08c13ef3..0000000000
--- a/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12875" ] || [ "$CI_BRANCH" = "master+about-print-all-arguments-names" ]; then
-
-    elpi_CI_REF=coq-master+adapt-coq12875-arguments-pass-name-impargs
-    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
deleted file mode 100644
index f0878202d3..0000000000
--- a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12892" ] || [ "$CI_BRANCH" = "update-s-univs" ]; then
-
-    elpi_CI_REF=update-s-univs
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-    equations_CI_REF=update-s-univs
-    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh
deleted file mode 100644
index ee75944a52..0000000000
--- a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12968" ] || [ "$CI_BRANCH" = "delay-frozen-evarconv" ]; then
-
-    equations_CI_REF=delay-frozen-evarconv
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh b/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh
deleted file mode 100644
index 7bed43afe1..0000000000
--- a/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12977" ] || [ "$CI_BRANCH" = "static-hint-poly" ]; then
-
-    equations_CI_REF=static-hint-poly
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-    fiat_parsers_CI_REF=static-hint-poly
-    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
-
-fi
diff --git a/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh b/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh
deleted file mode 100644
index 3407c2db39..0000000000
--- a/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "13028" ] || [ "$CI_BRANCH" = "master+fix-quotations-printing" ]; then
-
-    equations_CI_REF=master+adapt-coq-pr13028-quotation-qualifier-printing
-    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/13088-gares-par-to-tactic.sh b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh
deleted file mode 100644
index 4108a1aed1..0000000000
--- a/dev/ci/user-overlays/13088-gares-par-to-tactic.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "13088" ] || [ "$CI_BRANCH" = "par-to-tactic" ]; then
-
-    mtac2_CI_REF=par-to-tactic
-    mtac2_CI_GITURL=https://github.com/gares/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh
index 654d95f205..f16cf1497e 100644
--- a/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh
+++ b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh
@@ -1,6 +1,5 @@
 if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then
 
-    elpi_CI_REF=noinstance
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+    overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance
 
 fi
diff --git a/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh
deleted file mode 100644
index 1b3121781b..0000000000
--- a/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "13143" ] || [ "$CI_BRANCH" = "master+drop-misleading-arg-hbox" ]; then
-
-    aac_tactics_CI_REF=master+adapt-coq-pr13143-hbox-no-argument
-    aac_tactics_CI_GITURL=https://github.com/herbelin/aac-tactics
-
-    equations_CI_REF=master+adapt-coq-pr13143-hbox-no-argument
-    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
deleted file mode 100644
index 50eaf0b109..0000000000
--- a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then
-
-    elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation
-    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh b/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh
deleted file mode 100644
index 3b3b20baf1..0000000000
--- a/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8855" ] || [ "$CI_BRANCH" = "master+more-search-options" ]; then
-
-    coqhammer_CI_REF=master+adapt-pr8855-search-api
-    coqhammer_CI_GITURL=https://github.com/herbelin/coqhammer
-
-    coq_dpdgraph_CI_REF=coq-master+adapt-pr8855-search-api
-    coq_dpdgraph_CI_GITURL=https://github.com/herbelin/coq-dpdgraph
-
-fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 4c2f264a74..3f9ad5e878 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -4,15 +4,12 @@ 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`](../ci-basic-overlay.sh):
-give the name of your branch / commit using a `_CI_REF` variable and the
-location of your fork using a `_CI_GITURL` variable.
-The `_CI_GITURL` variable should be the URL of the repository without a
-trailing `.git`.
-If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is
-necessary to redefine the `_CI_ARCHIVEURL` variable as well.
+An overlay is a file which defines where to look for the patched
+version so that testing is possible. This is done by calling the
+`overlay` command for each project with the project name (as used in
+the variables in [`ci-basic-overlay.sh`](../ci-basic-overlay.sh)), the
+location of your fork and the branch containing the patch on your
+fork.
 
 Moreover, the file contains very simple logic to test the pull request number
 or branch name and apply it only in this case.
@@ -21,13 +18,12 @@ 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: `10185-SkySkimmer-instance-no-bang.sh` containing
+Example: `13128-SkySkimmer-noinstance.sh` containing
 
 ```
-if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then
+if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then
 
-    quickchick_CI_REF=instance-no-bang
-    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
+    overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance
 
 fi
 ```
diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh
index ad60b1115f..78ed27ba03 100755
--- a/dev/tools/create_overlays.sh
+++ b/dev/tools/create_overlays.sh
@@ -66,8 +66,7 @@ do
     make ci-$_CONTRIB_NAME || true
     setup_contrib_git $_CONTRIB_DIR $_CONTRIB_GITPUSHURL
 
-    echo "    ${_CONTRIB_NAME}_CI_REF=$OVERLAY_BRANCH" >> $OVERLAY_FILE
-    echo "    ${_CONTRIB_NAME}_CI_GITURL=$_CONTRIB_GITURL" >> $OVERLAY_FILE
+    echo "    overlay ${_CONTRIB_NAME} $_CONTRIB_GITURL $OVERLAY_BRANCH" >> $OVERLAY_FILE
     echo "" >> $OVERLAY_FILE
     shift
 done