8 files changed, 31 insertions, 37 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 0c8213b8f5..78c0b4b2c7 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1132,7 +1132,7 @@ function make_findlib {
 function make_dune {
   make_ocaml
 
-  if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 dune-1.6.3 ; then
+  if build_prep https://github.com/ocaml/dune/archive/ 1.10.0 tar.gz 1 dune-1.10.0 ; then
 
     log2 make release
     log2 make install
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/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/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/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 372e40a0b7..37c6e2f619 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -52,7 +52,7 @@ order to use them, do:
 
 ```
 $ make -f Makefile.dune voboot                # Only once per session
-$ dune exec dev/shim/coqtop-prelude
+$ dune exec -- dev/shim/coqtop-prelude
 ```
 
 or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets
@@ -108,14 +108,14 @@ automatically.
 You can use `ocamldebug` with Dune; after a build, do:
 
 ```
-dune exec dev/dune-dbg /path/to/foo.v
+dune exec -- dev/dune-dbg /path/to/foo.v
 (ocd) source dune_db
 ```
 
 or
 
 ```
-dune exec dev/dune-dbg checker Foo
+dune exec -- dev/dune-dbg checker Foo
 (ocd) source dune_db
 ```
 
@@ -130,7 +130,7 @@ For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`.
 
 After doing `make -f Makefile.dune voboot`, the following commands should work:
 ```
-dune exec dev/shim/coqbyte-prelude
+dune exec -- dev/shim/coqbyte-prelude
 > Drop.
 # #directory "dev";;
 # #use "include_dune";;
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index 8dfe1e7833..8736c0f9b8 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/bc9df0f66110039e495b6debe3a6cda4a1bb0fed.tar.gz";
-  sha256 = "0y2w259j0vqiwjhjvlbsaqnp1nl2zwz6sbwwhkrqn7k7fmhmxnq1";
+  url = "https://github.com/NixOS/nixpkgs/archive/31c38894c90429c9554eab1b416e59e3b6e054df.tar.gz";
+  sha256 = "1fv14rj5zslzm14ak4lvwqix94gm18h28376h4hsmrqqpnfqwsdw";
 })