diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 13 | ||||
| -rwxr-xr-x | dev/ci/gitlab.bat | 1 |
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 ^
|
