6 files changed, 6 insertions, 46 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/appveyor.sh b/dev/ci/appveyor.sh
deleted file mode 100644
index f26e0904bc..0000000000
--- a/dev/ci/appveyor.sh
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/bin/bash
-
-set -e -x
-
-APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c
-NJOBS=2
-
-wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
-tar -xf opam64.tar.xz
-bash opam64/install.sh
-
-opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing
-eval "$(opam env)"
-opam install -j $NJOBS -y num ocamlfind ounit
-
-# Full regular Coq Build
-cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index d39b92467d..95fceb773a 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 )
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 ^
diff --git a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
new file mode 100644
index 0000000000..0e1449f36c
--- /dev/null
+++ b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10069" ] || [ "$CI_BRANCH" = "whd-for-evar-conv-no-stack" ]; then
+
+    unicoq_CI_REF=whd-for-evar-conv-no-stack
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi