Remove old overlays

I updated the readme example using the most recent overlay with only 1
touched development.

33 files changed, 5 insertions, 339 deletions

diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh
deleted file mode 100644
index 2b4c1489ad..0000000000
--- a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-_OVERLAY_BRANCH=ho-matching-occ-sel
-
-if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    unicoq_CI_REF="PR7819-overlay"
-
-    mtac2_CI_REF="PR7819-overlay"
-    mtac2_CI_GITURL=https://github.com/mattam82/Mtac2
-
-    equations_CI_GITURL=https://github.com/mattam82/Coq-Equations
-    equations_CI_REF="PR7819-overlay"
-
-fi
diff --git a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
deleted file mode 100644
index 67f6f8610a..0000000000
--- a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
+++ /dev/null
@@ -1,18 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then
-
-    ltac2_CI_REF=master-parsing-decimal
-    ltac2_CI_GITURL=https://github.com/proux01/ltac2
-
-    quickchick_CI_REF=master-parsing-decimal
-    quickchick_CI_GITURL=https://github.com/proux01/QuickChick
-
-    Corn_CI_REF=master-parsing-decimal
-    Corn_CI_GITURL=https://github.com/proux01/corn
-
-    HoTT_CI_REF=master-parsing-decimal
-    HoTT_CI_GITURL=https://github.com/proux01/HoTT
-
-    stdlib2_CI_REF=master-parsing-decimal
-    stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
-
-fi
diff --git a/dev/ci/user-overlays/08817-sprop.sh b/dev/ci/user-overlays/08817-sprop.sh
deleted file mode 100644
index 81e18226ed..0000000000
--- a/dev/ci/user-overlays/08817-sprop.sh
+++ /dev/null
@@ -1,34 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8817" ] || [ "$CI_BRANCH" = "sprop" ]; then
-    aac_tactics_CI_REF=sprop
-    aac_tactics_CI_GITURL=https://github.com/SkySkimmer/aac-tactics
-
-    coq_dpdgraph_CI_REF=sprop
-    coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph
-
-    coqhammer_CI_REF=sprop
-    coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer
-
-    elpi_CI_REF=sprop
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-    equations_CI_REF=sprop
-    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    ltac2_CI_REF=sprop
-    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
-
-    unicoq_CI_REF=sprop
-    unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq
-
-    mtac2_CI_REF=sprop
-    mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2
-
-    paramcoq_CI_REF=sprop
-    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
-
-    quickchick_CI_REF=sprop
-    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
-
-    relation_algebra_CI_REF=sprop
-    relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra
-fi
diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh
deleted file mode 100644
index c04621114f..0000000000
--- a/dev/ci/user-overlays/08829-proj-syntax-check.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then
-    lambdaRust_CI_REF=proj-syntax-check
-    lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust
-    lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive
-fi
diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
deleted file mode 100644
index dc39ea5ef0..0000000000
--- a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then
-
-    equations_CI_BRANCH=master+fix-evars_of_term-pr8893
-    equations_CI_REF=master+fix-evars_of_term-pr8893
-    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
deleted file mode 100644
index 12be1b676a..0000000000
--- a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then
-
-    HoTT_CI_REF=rm-hardwired-hint-db
-    HoTT_CI_GITURL=https://github.com/vbgl/HoTT
-
-    ltac2_CI_REF=rm-hardwired-hint-db
-    ltac2_CI_GITURL=https://github.com/vbgl/ltac2
-
-    UniMath_CI_REF=rm-hardwired-hint-db
-    UniMath_CI_GITURL=https://github.com/vbgl/UniMath
-
-fi
diff --git a/dev/ci/user-overlays/08988-herbelin-master+mini-uniformizaton-parsing-printing-univ-level-sort.sh b/dev/ci/user-overlays/08988-herbelin-master+mini-uniformizaton-parsing-printing-univ-level-sort.sh
deleted file mode 100644
index ae72405e6e..0000000000
--- a/dev/ci/user-overlays/08988-herbelin-master+mini-uniformizaton-parsing-printing-univ-level-sort.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8988" ] || [ "$CI_BRANCH" = "master+mini-uniformizaton-parsing-printing-univ-level-sort" ]; then
-
-    elpi_CI_REF=coq-master+adapt-coq8988-type-internal-syntax
-    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh b/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh
deleted file mode 100644
index c09d1b8929..0000000000
--- a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9129" ] || [ "$CI_BRANCH" = "proof+no_global_partial" ]; then
-
-    aac_tactics_CI_REF=proof+no_global_partial
-    aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
-
-    # coqhammer_CI_REF=proof+no_global_partial
-    # coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer
-
-    elpi_CI_REF=proof+no_global_partial
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-    equations_CI_REF=proof+no_global_partial
-    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    ltac2_CI_REF=proof+no_global_partial
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    # unicoq_CI_REF=proof+no_global_partial
-    # unicoq_CI_GITURL=https://github.com/ejgallego/unicoq
-
-    mtac2_CI_REF=proof+no_global_partial
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-    paramcoq_CI_REF=proof+no_global_partial
-    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
-
-    quickchick_CI_REF=proof+no_global_partial
-    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh
deleted file mode 100644
index 1e1d36d54a..0000000000
--- a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then
-
-    elpi_CI_REF=recarg-cleanup
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-    quickchick_CI_REF=recarg-cleanup
-    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
deleted file mode 100644
index 23eb24c304..0000000000
--- a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then
-
-    ltac2_CI_REF=proofview+proof_info
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    fiat_parsers_CI_REF=proofview+proof_info
-    fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
-
-fi
diff --git a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh
deleted file mode 100644
index 1110157069..0000000000
--- a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9389" ] || [ "$CI_BRANCH" = "set-implicits" ]; then
-
-    equations_CI_REF=set-implicits
-    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    mtac2_CI_REF=set-implicits
-    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh
deleted file mode 100644
index cca85a2f68..0000000000
--- a/dev/ci/user-overlays/09439-sep-variance.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-
-if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then
-    elpi_CI_REF=sep-variance
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-    equations_CI_REF=sep-variance
-    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    mtac2_CI_REF=sep-variance
-    mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2
-
-    paramcoq_CI_REF=sep-variance
-    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
-fi
diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
deleted file mode 100644
index 1af8b5430d..0000000000
--- a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then
-
-    quickchick_CI_REF=context-constructor
-    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
-
-    equations_CI_REF=context-constructor
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh
deleted file mode 100644
index 27ce9aca16..0000000000
--- a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then
-
-    equations_CI_REF=hooks_unify
-    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    mtac2_CI_REF=hooks_unify
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-    paramcoq_CI_REF=hooks_unify
-    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
-
-fi
diff --git a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh
deleted file mode 100644
index 18a295cdbb..0000000000
--- a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9602" ] || [ "$CI_BRANCH" = "more-delta-in-termination-checking" ]; then
-
-    equations_CI_REF=more-delta-in-termination-checking
-    equations_CI_GITURL=https://github.com/gares/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/09678-printed-by-env.sh b/dev/ci/user-overlays/09678-printed-by-env.sh
deleted file mode 100644
index ccb3498764..0000000000
--- a/dev/ci/user-overlays/09678-printed-by-env.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-
-if [ "$CI_PULL_REQUEST" = "9678" ] || [ "$CI_BRANCH" = "printed-by-env" ]; then
-    elpi_CI_REF=printed-by-env
-    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
-
-    equations_CI_REF=printed-by-env
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-    ltac2_CI_REF=printed-by-env
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-    quickchick_CI_REF=printed-by-env
-    quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick
-fi
diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh
deleted file mode 100644
index b17454fc4c..0000000000
--- a/dev/ci/user-overlays/09733-gares-quotations.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then
-
-    ltac2_CI_REF=quotations
-    ltac2_CI_GITURL=https://github.com/gares/ltac2
-
-fi
diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh
deleted file mode 100644
index 4b49011de3..0000000000
--- a/dev/ci/user-overlays/09815-token-type.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then
-    ltac2_CI_REF=token-type
-    ltac2_CI_GITURL=https://github.com/proux01/ltac2
-fi
diff --git a/dev/ci/user-overlays/09870-vbgl-recordops.sh b/dev/ci/user-overlays/09870-vbgl-recordops.sh
deleted file mode 100644
index bb14a8c204..0000000000
--- a/dev/ci/user-overlays/09870-vbgl-recordops.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9870" ] || [ "$CI_BRANCH" = "doc-canonical" ]; then
-
-    elpi_CI_REF=pr-9870
-    elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh
deleted file mode 100644
index 9a42c829ce..0000000000
--- a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9895" ] || [ "$CI_BRANCH" = "require+upper" ]; then
-
-    quickchick_CI_REF=require+upper
-    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
deleted file mode 100644
index 01d3068591..0000000000
--- a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
+++ /dev/null
@@ -1,21 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then
-
-    elpi_CI_REF=pretyping-rm-global
-    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
-
-    coqhammer_CI_REF=pretyping-rm-global
-    coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer
-
-    equations_CI_REF=pretyping-rm-global
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-    ltac2_CI_REF=pretyping-rm-global
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-    paramcoq_CI_REF=pretyping-rm-global
-    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
-
-    mtac2_CI_REF=pretyping-rm-global
-    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh
deleted file mode 100644
index 9a6e25d893..0000000000
--- a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9973" ] || [ "$CI_BRANCH" = "elpi-1.2" ]; then
-
-    elpi_CI_REF=overlay-elpi1.2-coq-master
-    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh
deleted file mode 100644
index 9f9cc19e83..0000000000
--- a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10052" ] || [ "$CI_BRANCH" = "cleanup-logic-convert-hyp" ]; then
-
-    relation_algebra_CI_REF=cleanup-logic-convert-hyp
-    relation_algebra_CI_GITURL=https://github.com/ppedrot/relation-algebra
-
-fi
diff --git a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
deleted file mode 100644
index 0e1449f36c..0000000000
--- a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10069" ] || [ "$CI_BRANCH" = "whd-for-evar-conv-no-stack" ]; then
-
-    unicoq_CI_REF=whd-for-evar-conv-no-stack
-    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
-
-fi
diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
deleted file mode 100644
index 2015935dd9..0000000000
--- a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then
-
-    elpi_CI_REF=canonical-disable-hint
-    elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh
deleted file mode 100644
index 4032b1c6b5..0000000000
--- a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then
-
-    paramcoq_CI_REF=run_tactic_gen
-    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
-
-fi
diff --git a/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh b/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh
deleted file mode 100644
index 3658e96a3a..0000000000
--- a/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10133" ] || [ "$CI_BRANCH" = "kelim" ]; then
-
-    equations_CI_REF=kelim
-    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
deleted file mode 100644
index bc8aa33565..0000000000
--- a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then
-
-    unicoq_CI_REF=detype-anonymous
-    unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
-
-fi
diff --git a/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh b/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh
deleted file mode 100644
index fcbeb32a58..0000000000
--- a/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10188" ] || [ "$CI_BRANCH" = "def-not-visible-remove-warning" ]; then
-
-    elpi_CI_REF=def-not-visible-generic-warning
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh
deleted file mode 100644
index a89f6aca1b..0000000000
--- a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10177" ] || [ "$CI_BRANCH" = "generalize" ]; then
-
-    quickchick_CI_REF=generalize
-    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh b/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh
deleted file mode 100644
index e3bbb84bcb..0000000000
--- a/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10201" ] || [ "$CI_BRANCH" = "opaque-future-cleanup" ]; then
-
-    coq_dpdgraph_CI_REF=opaque-future-cleanup
-    coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph
-
-    coqhammer_CI_REF=opaque-future-cleanup
-    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
-
-    elpi_CI_REF=opaque-future-cleanup
-    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
-
-    paramcoq_CI_REF=opaque-future-cleanup
-    paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq
-
-fi
diff --git a/dev/ci/user-overlays/10215-gares-less-ontop.sh b/dev/ci/user-overlays/10215-gares-less-ontop.sh
deleted file mode 100644
index bceb5ad0e8..0000000000
--- a/dev/ci/user-overlays/10215-gares-less-ontop.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10215" ] || [ "$CI_BRANCH" = "custom-typing" ]; then
-
-    equations_CI_REF=pass-less-ontop
-    equations_CI_GITURL=https://github.com/gares/Coq-Equations
-
-    mtac2_CI_REF=pass-less-ontop
-    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
-
-    paramcoq_CI_REF=pass-less-ontop
-    paramcoq_CI_GITURL=https://github.com/gares/paramcoq
-
-    quickchick_CI_REF=pass-less-ontop
-    quickchick_CI_GITURL=https://github.com/gares/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 7fb73e447d..4c2f264a74 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -21,14 +21,14 @@ 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
+Example: `10185-SkySkimmer-instance-no-bang.sh` containing
 
 ```
-#!/bin/sh
+if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then
+
+    quickchick_CI_REF=instance-no-bang
+    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
 
-if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
-    mathcomp_CI_REF=ssr-merge
-    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp
 fi
 ```