15 files changed, 64 insertions, 42 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/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
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/doc/critical-bugs b/dev/doc/critical-bugs
index 01c2b574a2..d00c8cb11a 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -119,6 +119,16 @@ Universes
   GH issue number: #8341
   risk: unlikely to be activated by chance (requires a plugin)
 
+  component: template polymorphism
+  summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though)
+  impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found
+  impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit)
+  fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau)
+  found by: Gilbert using explicit sharing of universes, exploit found for 8.5-8.9 by Pédrot, other variants generating sharing using sections, or using ltac tricks by Sozeau, exploit in 8.4 by Herbelin and Jason Gross by adding new tricks to Sozeau's variants
+  exploit: test-suite/failure/Template.v
+  GH issue number: #9294
+  risk: moderate risk to be activated by chance
+
 Primitive projections
 
   component: primitive projections, guard condition
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index c7f36ee964..7e53f13e45 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -3,5 +3,5 @@
 ; Add custom flags here. Default developer profile is `dev`
 (context (opam (switch 4.05.0)))
 (context (opam (switch 4.05.0+32bit)))
-(context (opam (switch 4.08.0)))
-(context (opam (switch 4.08.0+flambda)))
+(context (opam (switch 4.08.1)))
+(context (opam (switch 4.08.1+flambda)))
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";
 })