10 files changed, 45 insertions, 33 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 408d36df7f..9ed7180807 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -120,15 +120,18 @@ Currently available artifacts are:
   Additionally, an experimental Dune build is provided:
   https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev
 
-- the Coq documentation, built in the `doc:*` jobs. When submitting
-  a documentation PR, this can help reviewers checking the rendered result:
-
-  + Coq's Reference Manual [master branch]
-    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
-  + Coq's Standard Library Documentation [master branch]
-    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base
-  + Coq's ML API Documentation [master branch]
-    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
+- the Coq documentation, built in the `doc:*` jobs. When submitting a
+  documentation PR, this can help reviewers checking the rendered
+  result.  **@coqbot** will automatically post links to these
+  artifacts in the PR checks section.  Furthemore, these artifacts are
+  automatically deployed at:
+
+  + Coq's Reference Manual [master branch]:
+    <https://coq.github.io/doc/master/refman/>
+  + Coq's Standard Library Documentation [master branch]:
+    <https://coq.github.io/doc/master/stdlib/>
+  + Coq's ML API Documentation [master branch]:
+    <https://coq.github.io/doc/master/api/>
 
 ### GitLab and Windows
 
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 34d748e1cc..03ce5a6b5d 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -2,7 +2,7 @@
 
 set -e -x
 
-OPAM_VARIANT=ocaml-variants.4.08.0+mingw64c
+OPAM_VARIANT=ocaml-variants.4.08.1+mingw64c
 
 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
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index ad22c394d8..3923fea30e 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -56,14 +56,14 @@
 
 # NB: stdpp and Iris refs are gotten from the opam files in the Iris
 # and lambdaRust repos respectively.
-: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}"
+: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}"
 : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
 
-: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}"
+: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
 : "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
 
 : "${lambdaRust_CI_REF:=master}"
-: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}"
+: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
 : "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}"
 
 ########################################################################
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
deleted file mode 100755
index ca759c7b39..0000000000
--- a/dev/ci/ci-cpdt.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-wget http://adam.chlipala.net/cpdt/cpdt.tgz
-tar xvfz cpdt.tgz
-
-( cd cpdt && make clean && make )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
deleted file mode 100755
index a2f0bea555..0000000000
--- a/dev/ci/ci-tlc.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-FORCE_GIT=1
-git_download tlc
-
-( cd "${CI_BUILD_DIR}/tlc" && make )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 011c7fbdec..7175b5ffd5 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-07-06-V22"
+# CACHEKEY: "bionic_coq-V2019-08-08-V01"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.08.0" \
+ENV COMPILER_EDGE="4.08.1" \
     COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \
     BASE_OPAM_EDGE="dune-release.1.3.1"
 
diff --git a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh
new file mode 100644
index 0000000000..413805e8e9
--- /dev/null
+++ b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10642" ] || [ "$CI_BRANCH" = "feedback-added-axiom" ]; then
+
+    elpi_CI_REF=feedback-added-axiom
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh
new file mode 100644
index 0000000000..21ff60493b
--- /dev/null
+++ b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10660" ] || [ "$CI_BRANCH" = "errors+private" ]; then
+
+    coqhammer_CI_REF=errors+private
+    coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer
+
+fi
diff --git a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh
new file mode 100644
index 0000000000..0c47f6a60b
--- /dev/null
+++ b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10665" ] || [ "$CI_BRANCH" = "api+varkind" ]; then
+
+    elpi_CI_REF=api+varkind
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    quickchick_CI_REF=api+varkind
+    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh
new file mode 100644
index 0000000000..6dc44aa627
--- /dev/null
+++ b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then
+
+    equations_CI_REF=proofs+declare_unif
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi