3 files changed, 18 insertions, 2 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5c37b3133e..cb1493d6aa 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -53,6 +53,12 @@
 : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
 
 ########################################################################
+# Ltac2
+########################################################################
+: ${ltac2_CI_BRANCH:=master}
+: ${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}
+
+########################################################################
 # GeoCoq
 ########################################################################
 : ${GeoCoq_CI_BRANCH:=master}
@@ -80,7 +86,7 @@
 # VST
 ########################################################################
 : ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/Zimmi48/VST.git}
+: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
 
 ########################################################################
 # fiat_parsers
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index ff5935d4c7..d68674381a 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
 
 # This script could be included inside other ones
 # Let's avoid to source ci-common twice in this case
-if [ -z "${CI_BUILD_DIR}"];
+if [ -z "${CI_BUILD_DIR}" ];
 then
     source ${ci_dir}/ci-common.sh
 fi
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
new file mode 100755
index 0000000000..4865be31ec
--- /dev/null
+++ b/dev/ci/ci-ltac2.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
+
+git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR}
+
+( cd ${ltac2_CI_DIR} && make -j ${NJOBS} && make tests && make install )