7 files changed, 26 insertions, 10 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 45176581cd..43d680af61 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -75,9 +75,6 @@ We are currently running tests on the following platforms:
   camlp5, and with warnings as errors; it runs the test-suite and tests the
   compilation of several external developments.
 
-- Circle CI runs tests that are redundant with GitLab CI and may be removed
-  eventually.
-
 - Travis CI is used to test the compilation of Coq and run the test-suite on
   macOS. It also runs a linter that checks whitespace discipline. A
   [pre-commit hook](../tools/pre-commit) is automatically installed by
@@ -165,8 +162,7 @@ automatically built and uploaded to your GitLab registry, and is
 loaded by subsequent jobs.
 
 **IMPORTANT**: When updating Coq's CI docker image, you must modify
-the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml),
-[`.circleci/config.yml`](../../.circleci/config.yml),
+the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml)
 and [`Dockerfile`](docker/bionic_coq/Dockerfile)
 
 The Docker building job reuses the uploaded image if it is available,
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index a68cd0933e..9259a6e0c8 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -20,10 +20,6 @@ else
     then
         export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
         export CI_BRANCH="$TRAVIS_BRANCH"
-    elif [ -n "${CIRCLECI}" ];
-    then
-        export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
-        export CI_BRANCH="$CIRCLE_BRANCH"
     else # assume local
         CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
         export CI_BRANCH
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 6ded97984e..184b90a50b 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT
 
 git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}"
 
-( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make )
+( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate )
diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh
new file mode 100644
index 0000000000..27f588e214
--- /dev/null
+++ b/dev/ci/user-overlays/07859-printers.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then
+    Equations_CI_BRANCH=fix-printers
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/07908-proj-mind.sh b/dev/ci/user-overlays/07908-proj-mind.sh
new file mode 100644
index 0000000000..293eeb5a5a
--- /dev/null
+++ b/dev/ci/user-overlays/07908-proj-mind.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7908" ] || [ "$CI_BRANCH" = "proj-mind" ]; then
+    Equations_CI_BRANCH=fix-proj-mind
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh
new file mode 100644
index 0000000000..56c0dc3433
--- /dev/null
+++ b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7941" ] || [ "$CI_BRANCH" = "jun-27-missing-record-field-error-message-quickfix" ]; then
+    Equations_CI_BRANCH=overlay-question-mark-extended-for-missing-record-field
+    Equations_CI_GITURL=https://github.com/bollu/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
new file mode 100644
index 0000000000..99a11b9fbf
--- /dev/null
+++ b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8063" ] || [ "$CI_BRANCH" = "string-eqb" ]; then
+    quickchick_CI_BRANCH=fix-for-pr-8063
+    quickchick_CI_GITURL=https://github.com/JasonGross/QuickChick
+fi