5 files changed, 33 insertions, 8 deletions
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/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh
new file mode 100644
index 0000000000..7d55cf6883
--- /dev/null
+++ b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13166" ] || [ "$CI_BRANCH" = "master+fixes13165-missing-impargs-defined-fields" ]; then
+
+    elpi_CI_REF=coq-master+adapt-coq-pr13166-impargs-record-fields
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fb5d7cc244..6a6318f97a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,22 +1,35 @@
 ## Changes between Coq 8.12 and Coq 8.13
 
-- Tactic language: TacGeneric now takes an argument to tell if it
-  comes from a notation. Use `None` if not and `Some foo` to tell to
-  print such TacGeneric surrounded with `foo:( )`.
-
 ### Code formatting
 
 - The automatic code formatting tool `ocamlformat` has been disabled and its
   git hook removed. If desired, automatic formatting can be achieved by calling
   the `fmt` target of the dune build system.
 
-### Pp library
+### ML API
+
+Abstract syntax of tactic:
+
+- TacGeneric now takes an argument to tell if it comes from a
+  notation. Use `None` if not and `Some foo` to tell to print such
+  TacGeneric surrounded with `foo:( )`.
+
+Printing functions:
 
 - `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`.
 
+Grammar entries:
+
+- `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident`
+  which now returns a located identifier.
+
+Generic arguments:
+
+- Generic arguments: `wit_var` is deprecated, use `wit_hyp`.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting