4 files changed, 22 insertions, 1 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index bd7ee46358..70e3fe5c69 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -330,3 +330,10 @@
 : "${perennial_CI_REF:=master}"
 : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
 : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
+
+########################################################################
+# metacoq
+########################################################################
+: "${metacoq_CI_REF:=master}"
+: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
+: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 871d033f5b..30047e624b 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download equations
 
-( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci)
+( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..1302065961
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download metacoq
+
+( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install )
diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
new file mode 100644
index 0000000000..8a734feada
--- /dev/null
+++ b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then
+
+    quickchick_CI_REF=master+adapting-numTok-new-api-pr11703
+    quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
+
+fi