7 files changed, 34 insertions, 3 deletions
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index 7625e4e7f7..41f204385f 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -428,6 +428,9 @@ for coq_opam_package in $sorted_coq_opam_packages; do
     new_base_path=$new_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/
     old_base_path=$old_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/
     for vo in `cd $new_opam_root/$new_base_path/; find -name '*.vo'`; do
+        if [ -e $old_opam_root/$old_base_path/$vo ]; then
+          echo "$coq_opam_package/$vo $(stat -c%s $old_opam_root/$old_base_path/$vo) $(stat -c%s $new_opam_root/$new_base_path/$vo)" >> "$log_dir/vosize.log"
+        fi
         if [ -e $old_opam_root/$old_base_path/${vo%%o}.timing -a \
                 -e $new_opam_root/$new_base_path/${vo%%o}.timing ]; then
             mkdir -p $working_dir/html/$coq_opam_package/`dirname $vo`/
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index fcc585117b..fc8921e63d 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1204,7 +1204,7 @@ function make_elpi {
   make_dune
   make_re
 
-  if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz 1 elpi; then
+  if build_prep https://github.com/LPCIC/elpi/archive v1.11.4 tar.gz 1 elpi; then
 
     log2 dune build -p elpi
     log2 dune install elpi
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index f672ead807..c17ec502e7 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-09-17-V88"
+# CACHEKEY: "bionic_coq-V2020-10-12-V89"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -43,7 +43,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages
 ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.11.0"
+    BASE_ONLY_OPAM="elpi.1.11.4"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
diff --git a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh
new file mode 100644
index 0000000000..fb5947d218
--- /dev/null
+++ b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12449" ] || [ "$CI_BRANCH" = "minim-prop-toset" ]; then
+
+    mtac2_CI_REF=janno/coq-12449
+    mtac2_CI_GITURL=https://github.com/mtac2/mtac2
+
+fi
diff --git a/dev/ci/user-overlays/13088-gares-par-to-tactic.sh b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh
new file mode 100644
index 0000000000..4108a1aed1
--- /dev/null
+++ b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13088" ] || [ "$CI_BRANCH" = "par-to-tactic" ]; then
+
+    mtac2_CI_REF=par-to-tactic
+    mtac2_CI_GITURL=https://github.com/gares/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh
new file mode 100644
index 0000000000..1b3121781b
--- /dev/null
+++ b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "13143" ] || [ "$CI_BRANCH" = "master+drop-misleading-arg-hbox" ]; then
+
+    aac_tactics_CI_REF=master+adapt-coq-pr13143-hbox-no-argument
+    aac_tactics_CI_GITURL=https://github.com/herbelin/aac-tactics
+
+    equations_CI_REF=master+adapt-coq-pr13143-hbox-no-argument
+    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 59c1623a2d..fb5d7cc244 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -10,6 +10,13 @@
   git hook removed. If desired, automatic formatting can be achieved by calling
   the `fmt` target of the dune build system.
 
+### Pp library
+
+- `Pp.h` does not take a `int` argument anymore (the argument was
+  not used). In general, where `h n` for `n` non zero was used, `hv n`
+  was instead intended. If cancelling the breaking role of cuts in the
+  box was intended, turn `h n c` into `h c`.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting