aboutsummaryrefslogtreecommitdiff
path: root/dev/build
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-08 20:40:19 +0200
committerThéo Zimmermann2019-05-08 20:40:19 +0200
commit053e64206aa70c6a12c75b59e8267eeaba00d1ce (patch)
treeca27106456f7643b08ee328f34628e999d222dd1 /dev/build
parent928bced545407a2043fe2acaa5b31b1aa07988d5 (diff)
Remove ltac2 add-on from Windows installer now that it is in the main Coq package.
Diffstat (limited to 'dev/build')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh13
1 files changed, 0 insertions, 13 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 {