Merge PR #9153: [api] Move reduction modules to `tactics`

12 files changed, 0 insertions, 107 deletions

diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh
deleted file mode 100644
index b05d02c5be..0000000000
--- a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-_OVERLAY_BRANCH=clean-transp-state
-
-if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    unicoq_CI_REF="$_OVERLAY_BRANCH"
-    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
-
-    equations_CI_REF="$_OVERLAY_BRANCH"
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-    mtac2_CI_REF="$_OVERLAY_BRANCH"
-    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh
deleted file mode 100644
index 3600f1cd3e..0000000000
--- a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh
+++ /dev/null
@@ -1,18 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8705" ] || [ "$CI_BRANCH" = "vernac+remove_empty_hooks" ]; then
-
-    elpi_CI_REF=vernac+remove_empty_hooks
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-    equations_CI_REF=vernac+remove_empty_hooks
-    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    paramcoq_CI_REF=vernac+remove_empty_hooks
-    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
-
-    plugin_tutorial_CI_REF=vernac+remove_empty_hooks
-    plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
-
-    mtac2_CI_REF=vernac+remove_empty_hooks
-    mtac2_CI_GITURL=https://github.com/ejgallego/mtac2
-
-fi
diff --git a/dev/ci/user-overlays/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh
deleted file mode 100644
index 482792d7cd..0000000000
--- a/dev/ci/user-overlays/08850-poly-local-univs.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/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
diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh
deleted file mode 100644
index 17eb5fffae..0000000000
--- a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then
-
-    Equations_CI_REF=program-hook-obligation-subst
-    Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh
deleted file mode 100644
index 08112d3054..0000000000
--- a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then
-
-    aactactics_CI_REF=ltac+use_atts_in_ast
-    aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
-
-    coqhammer_CI_REF=ltac+use_atts_in_ast
-    coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer
-
-    Equations_CI_REF=ltac+use_atts_in_ast
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    mtac2_CI_REF=ltac+use_atts_in_ast
-    mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh
deleted file mode 100644
index 1c5157ba12..0000000000
--- a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then
-
-    quickchick_CI_REF=lib+better_boot_coqproject
-    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh
deleted file mode 100644
index e74e53fa40..0000000000
--- a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8933" ] || [ "$CI_BRANCH" = "solve-remaining-evars-initial-arg" ]; then
-    plugin_tutorial_CI_REF=solve-remaining-evars-initial-arg
-    plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials
-fi
diff --git a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh
deleted file mode 100644
index d7130cc67a..0000000000
--- a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8985" ] || [ "$CI_BRANCH" = "build+pack_gramlib" ]; then
-
-    elpi_CI_REF=use_coq_gramlib
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
deleted file mode 100644
index c8bea0c868..0000000000
--- a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then
-
-    equations_CI_REF=legacy_proof_eng_clean
-    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh
deleted file mode 100644
index 61ffa4a197..0000000000
--- a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then
-
-    ltac2_CI_REF=vernac+move_extend_ast
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-fi
diff --git a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh
deleted file mode 100644
index 14e7c0d7f0..0000000000
--- a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9051" ] || [ "$CI_BRANCH" = "camlp5-safe-api-strikes-back" ]; then
-
-    equations_CI_REF=camlp5-safe-api-strikes-back
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-    ltac2_CI_REF=camlp5-safe-api-strikes-back
-    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
-
-fi
diff --git a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh
deleted file mode 100644
index e9daa7a44e..0000000000
--- a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9065" ] || [ "$CI_BRANCH" = "gramlib+no_ploc" ]; then
-
-    elpi_CI_REF=gramlib+no_ploc
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi