8 files changed, 36 insertions, 18 deletions
diff --git a/dev/base_include b/dev/base_include
index b30bbaa3fa..4841db8953 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -134,7 +134,6 @@ open Tacticals
 open Tactics
 open Eqschemes
 
-open ExplainErr
 open Class
 open ComDefinition
 open Indschemes
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 9448a03f4f..34d748e1cc 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.07.1+mingw64c
+OPAM_VARIANT=ocaml-variants.4.08.0+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/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index f07a5cdb98..011c7fbdec 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-06-21-V1"
+# CACHEKEY: "bionic_coq-V2019-07-06-V22"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
                  antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.4/opam-2.0.4-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -37,8 +37,9 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
-    CI_OPAM="menhir.20181113 elpi.1.4.0 ocamlgraph.1.8.8"
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.10.0 ounit.2.0.8 odoc.1.4.0" \
+    CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
+    BASE_ONLY_OPAM="elpi.1.4.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
@@ -48,16 +49,16 @@ ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
-    opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM
+    opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM
 
 # base+32bit switch
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.07.1" \
-    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" \
-    BASE_OPAM_EDGE="dune-release.1.1.0"
+ENV COMPILER_EDGE="4.08.0" \
+    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \
+    BASE_OPAM_EDGE="dune-release.1.3.1"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/ci/user-overlays/10419-ejgallego-heads+test.sh b/dev/ci/user-overlays/10419-ejgallego-heads+test.sh
new file mode 100644
index 0000000000..0ec0c3673a
--- /dev/null
+++ b/dev/ci/user-overlays/10419-ejgallego-heads+test.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "10419" ] || [ "$CI_BRANCH" = "heads+test" ]; then
+
+    elpi_CI_REF=heads+test
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    equations_CI_REF=heads+test
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    mtac2_CI_REF=heads+test
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    paramcoq_CI_REF=heads+test
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    quickchick_CI_REF=heads+test
+    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index cf95941de5..c7f36ee964 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.07.1)))
-(context (opam (switch 4.07.1+flambda)))
+(context (opam (switch 4.08.0)))
+(context (opam (switch 4.08.0+flambda)))
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 425f21de70..c0a3eeb11c 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -209,7 +209,8 @@ has_state() {
     [ "$(jq -rc 'map(select(.user.login == "'"$1"'") | .state) | any(. == "'"$2"'")' <<< "$reviews")" = true ]
 }
 
-for reviewer in $(jq -rc 'map(.user.login) | unique | join(" ")' <<< "$reviews" ); do
+author=$(echo "$PRDATA" | jq -rc '.user.login')
+for reviewer in $(jq -rc 'map(.user.login | select(. != "'"$author"'")) | unique | join(" ")' <<< "$reviews" ); do
     if has_state "$reviewer" APPROVED; then
         msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Reviewed-by="$reviewer")
     elif has_state "$reviewer" COMMENTED; then
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 0338cd42c7..c7bb36b6d3 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python2
 from __future__ import with_statement
 import os, re, sys, subprocess
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8343853af5..aa28bce018 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -15,7 +15,6 @@ open Util
 open Pp
 open Names
 open Libnames
-open Globnames
 open Univ
 open Environ
 open Printer
@@ -141,7 +140,7 @@ let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x)
 
 let pP s = pp (hov 0 s)
 
-let safe_pr_global = function
+let safe_pr_global = let open GlobRef in function
   | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")")
   | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
 			  int i ++ str ")")
@@ -558,7 +557,7 @@ let encode_path ?loc prefix mpdir suffix id =
   make_qualid ?loc
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
-let raw_string_of_ref ?loc _ = function
+let raw_string_of_ref ?loc _ = let open GlobRef in function
   | ConstRef cst ->
       let (mp,id) = Constant.repr2 cst in
       encode_path ?loc "CST" (Some mp) [] (Label.to_id id)
@@ -574,7 +573,7 @@ let raw_string_of_ref ?loc _ = function
   | VarRef id ->
       encode_path ?loc "SECVAR" None [] id
 
-let short_string_of_ref ?loc _ = function
+let short_string_of_ref ?loc _ = let open GlobRef in function
   | VarRef id -> qualid_of_ident ?loc id
   | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (Constant.label cst))
   | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (MutInd.label kn))