[ci] Cleanup of old overlays.

17 files changed, 0 insertions, 139 deletions

diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
deleted file mode 100644
index d812df3ec0..0000000000
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-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
diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh
deleted file mode 100644
index 575df07425..0000000000
--- a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-_OVERLAY_BRANCH=pure-sharing-flag
-
-if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
-    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh
deleted file mode 100644
index 019cb8054d..0000000000
--- a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then
-    cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification
-    cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto
-fi
diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh
deleted file mode 100644
index 3a6480a5a1..0000000000
--- a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then
-
-    ltac2_CI_BRANCH=master+globenv-coq-pr7288
-    ltac2_CI_GITURL=https://github.com/herbelin/ltac2
-
-fi
diff --git a/dev/ci/user-overlays/08456-fix-6764.sh b/dev/ci/user-overlays/08456-fix-6764.sh
deleted file mode 100644
index 3b951d9c07..0000000000
--- a/dev/ci/user-overlays/08456-fix-6764.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8456" ] || [ "$CI_BRANCH" = "fix-6764" ]; then
-    Elpi_CI_REF=overlay/8456
-fi
diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh
deleted file mode 100755
index 4605255d5e..0000000000
--- a/dev/ci/user-overlays/08515-command-atts.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then
-    ltac2_CI_REF=command-atts
-    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
-
-    Equations_CI_REF=command-atts
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    plugin_tutorial_CI_REF=command-atts
-    plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials
-fi
diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh
deleted file mode 100644
index c08f44fc50..0000000000
--- a/dev/ci/user-overlays/08552-gares-elpi-11.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then
-    Elpi_CI_REF=coq-master-elpi-1.1
-fi
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
deleted file mode 100644
index 484ad8f9e6..0000000000
--- a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-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
deleted file mode 100644
index 41c2ad6fef..0000000000
--- a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-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
diff --git a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh
deleted file mode 100644
index 9d723dc7f2..0000000000
--- a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-_OVERLAY_BRANCH=name-abstract-univ-context
-
-if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    Elpi_CI_REF="$_OVERLAY_BRANCH"
-    Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
-
-    Equations_CI_REF="$_OVERLAY_BRANCH"
-    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
deleted file mode 100644
index bd3e1bf7ff..0000000000
--- a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then
-    plugin_tutorial_CI_REF=pr8671-fix
-    plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials
-
-fi
diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
deleted file mode 100644
index 98530c825a..0000000000
--- a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then
-
-    Elpi_CI_REF=kernel-entries-cleanup
-    Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
-
-    Equations_CI_REF=kernel-entries-cleanup
-    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
deleted file mode 100644
index 81ed91f52b..0000000000
--- a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then
-
-    Elpi_CI_REF=master+generalized-evar-printers-pr8688
-    Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
deleted file mode 100644
index b3a9f67e00..0000000000
--- a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then
-
-    # ltac2_CI_REF=rm-section-path
-    # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-    plugin_tutorial_CI_REF=vernac+monify_hook
-    plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
-
-    Elpi_CI_REF=vernac+monify_hook
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-    Equations_CI_REF=vernac+monify_hook
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh b/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh
deleted file mode 100644
index 4536c62c64..0000000000
--- a/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-_OVERLAY_BRANCH=rm-implicit-tactic
-
-if [ "$CI_PULL_REQUEST" = "8779" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    ltac2_CI_REF="$_OVERLAY_BRANCH"
-    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
-
-fi
diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh
deleted file mode 100644
index 8ad8cba243..0000000000
--- a/dev/ci/user-overlays/08844-split-tactics.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then
-    Equations_CI_REF=split-tactics
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    ltac2_CI_REF=split-tactics
-    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
-
-    fiat_parsers_CI_REF=split-tactics
-    fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat
-fi
diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
deleted file mode 100644
index 76aa37d380..0000000000
--- a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then
-    HoTT_CI_REF=fix-for-numeral-notations
-    HoTT_CI_GITURL=https://github.com/JasonGross/HoTT
-    HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive
-fi