9 files changed, 9 insertions, 61 deletions
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh
index ac74ebf667..ac74ebf667 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat_parsers.sh
diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
deleted file mode 100644
index 6e89741e29..0000000000
--- a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then
-
-    bignums_CI_REF=primitive-integers
-    bignums_CI_GITURL=https://github.com/vbgl/bignums
-
-    mtac2_CI_REF=primitive-integers
-    mtac2_CI_GITURL=https://github.com/vbgl/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
deleted file mode 100644
index 2df8affd14..0000000000
--- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then
-
-    elpi_CI_REF=ltac+remove_aliases
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
deleted file mode 100644
index f2a113b118..0000000000
--- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then
-
-    mtac2_CI_REF=build+warn_50
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
deleted file mode 100644
index f532fdfc52..0000000000
--- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then
-
-    ltac2_CI_REF=proof_rework
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    mtac2_CI_REF=proof_rework
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-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
new file mode 100644
index 0000000000..23eb24c304
--- /dev/null
+++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
@@ -0,0 +1,9 @@
+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/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
deleted file mode 100644
index efcdd2e97f..0000000000
--- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then
-
-    paramcoq_CI_REF=stm-shallow-logic
-    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
-
-fi
diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
deleted file mode 100644
index ebd1b524da..0000000000
--- a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then
-
-    mtac2_CI_REF=proof-mode
-    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
-
-    ltac2_CI_REF=proof-mode
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-    equations_CI_REF=proof-mode
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh
deleted file mode 100644
index 985c2db74e..0000000000
--- a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9410" ] || [ "$CI_BRANCH" = "thread-program" ]; then
-
-    math_classes_CI_REF=program-mode-flag
-    math_classes_CI_GITURL=https://github.com/maximedenes/math-classes
-
-    ltac2_CI_REF=program-mode-flag
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-
-    equations_CI_REF=thread-program
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi