Remove ltac2 add-on from Windows installer now that it is in the main Coq package.

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 ^