Remove ppedrot/ltac2 from CI after integration in main repo

4 files changed, 0 insertions, 19 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2bfb91f27f..e4815920ce 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -638,9 +638,6 @@ plugin:ci-equations:
 plugin:ci-fiat_parsers:
   extends: .ci-template
 
-plugin:ci-ltac2:
-  extends: .ci-template
-
 plugin:ci-mtac2:
   extends: .ci-template
 
diff --git a/Makefile.ci b/Makefile.ci
index a244c17ef3..95ebd64ba1 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -32,7 +32,6 @@ CI_TARGETS= \
     ci-coqhammer \
     ci-hott \
     ci-iris-lambda-rust \
-    ci-ltac2 \
     ci-math-classes \
     ci-math-comp \
     ci-mtac2 \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4f5988c59c..f97e781832 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -81,13 +81,6 @@
 : "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}"
 
 ########################################################################
-# Ltac2
-########################################################################
-: "${ltac2_CI_REF:=master}"
-: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}"
-: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}"
-
-########################################################################
 # GeoCoq
 ########################################################################
 : "${GeoCoq_CI_REF:=master}"
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
deleted file mode 100755
index 4df22bf249..0000000000
--- a/dev/ci/ci-ltac2.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download ltac2
-
-( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install )