aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh13
-rwxr-xr-xdev/ci/gitlab.bat1
2 files changed, 0 insertions, 14 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index ea9af60330..d737632638 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1630,19 +1630,6 @@ function make_addon_ssreflect {
fi
}
-# Ltac-2 plugin
-# A new (experimental) tactic language
-
-function make_addon_ltac2 {
- installer_addon_dependency ltac2
- if build_prep_overlay ltac2; then
- installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" ""
- log1 make $MAKE_OPT all
- log2 make install
- build_post
- fi
-}
-
# UniCoq plugin
# An alternative unification algorithm
function make_addon_unicoq {
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index cc1931d13d..6c4ccfc14d 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -41,7 +41,6 @@ IF "%WINDOWS%" == "enabled_all_addons" (
SET EXTRA_ADDONS=^
-addon=bignums ^
-addon=equations ^
- -addon=ltac2 ^
-addon=mtac2 ^
-addon=mathcomp ^
-addon=menhir ^