15 files changed, 88 insertions, 60 deletions
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml
index 4275e3d121..25545cf565 100644
--- a/dev/bench/gitlab-bench.yml
+++ b/dev/bench/gitlab-bench.yml
@@ -11,18 +11,6 @@ bench:
     - timing
   variables:
     GIT_DEPTH: ""
-    coq_pr_number: ""
-    coq_pr_comment_id: ""
-    new_ocaml_switch: "ocaml-base-compiler.4.07.1"
-    old_ocaml_switch: "ocaml-base-compiler.4.07.1"
-    new_coq_repository: "https://gitlab.com/coq/coq.git"
-    old_coq_repository: "https://gitlab.com/coq/coq.git"
-    new_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git"
-    old_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git"
-    new_coq_opam_archive_git_branch: "master"
-    old_coq_opam_archive_git_branch: "master"
-    num_of_iterations: 1
-    coq_opam_packages: "coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast"
   artifacts:
     name: "$CI_JOB_NAME"
     paths:
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index 7625e4e7f7..1dea97160c 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -40,18 +40,19 @@ echo $PWD
 #check_variable "JOB_NAME"
 #check_variable "JENKINS_URL"
 check_variable "CI_JOB_URL"
-check_variable "coq_pr_number"
-check_variable "coq_pr_comment_id"
-check_variable "new_ocaml_switch"
-check_variable "new_coq_repository"
-check_variable "new_coq_opam_archive_git_uri"
-check_variable "new_coq_opam_archive_git_branch"
-check_variable "old_ocaml_switch"
-check_variable "old_coq_repository"
-check_variable "old_coq_opam_archive_git_uri"
-check_variable "old_coq_opam_archive_git_branch"
-check_variable "num_of_iterations"
-check_variable "coq_opam_packages"
+
+: "${coq_pr_number:=''}"
+: "${coq_pr_comment_id:=''}"
+: "${new_ocaml_switch:='ocaml-base-compiler.4.07.1'}"
+: "${old_ocaml_switch:='ocaml-base-compiler.4.07.1'}"
+: "${new_coq_repository:='https://gitlab.com/coq/coq.git'}"
+: "${old_coq_repository:='https://gitlab.com/coq/coq.git'}"
+: "${new_coq_opam_archive_git_uri:='https://github.com/coq/opam-coq-archive.git'}"
+: "${old_coq_opam_archive_git_uri:='https://github.com/coq/opam-coq-archive.git'}"
+: "${new_coq_opam_archive_git_branch:='master'}"
+: "${old_coq_opam_archive_git_branch:='master'}"
+: "${num_of_iterations:=1}"
+: "${coq_opam_packages:='coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast'}"
 
 new_coq_commit=$(git rev-parse HEAD^2)
 old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit)
@@ -428,6 +429,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/ci-iris.sh b/dev/ci/ci-iris.sh
index 0256906112..9616f3ce00 100755
--- a/dev/ci/ci-iris.sh
+++ b/dev/ci/ci-iris.sh
@@ -9,13 +9,13 @@ git_download iris_string_ident
 git_download iris_examples
 
 # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
-iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/coq-iris-examples.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
 
 # Setup Iris
 git_download iris
 
 # Extract required version of std++
-stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/coq-iris.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
 
 # Setup std++
 git_download stdpp
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/13128-SkySkimmer-noinstance.sh b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh
new file mode 100644
index 0000000000..654d95f205
--- /dev/null
+++ b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then
+
+    elpi_CI_REF=noinstance
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+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/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 7d2100515d..6a6318f97a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,8 +1,34 @@
 ## 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.
+
+### 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
 
diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md
index f8b4537e77..4982e3e94d 100644
--- a/dev/doc/parsing.md
+++ b/dev/doc/parsing.md
@@ -73,7 +73,7 @@ very specific to Coq (not so similar to Camlp5):
   END
   ```
 
-  Global nonterminals are declared in `pcoq.ml`, e.g. `let bignat = Entry.create "Prim.bignat"`.
+  Global nonterminals are declared in `pcoq.ml`, e.g. `let bignat = Entry.create "bignat"`.
   All the `*.mlg` files include `open Pcoq` and often its modules, e.g. `open Pcoq.Prim`.
 
   `GRAMMAR EXTEND` should be used only for large syntax additions.  To add new commands
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 553696410c..2e8a7455de 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -32,7 +32,4 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 |
 echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
-echo Checking ocamlformat
-make -f Makefile.dune fmt || CODE=1
-
 exit $CODE
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 91cb6168e1..534f20f85b 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -30,7 +30,7 @@ exec $OCAMLDEBUG \
     -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
     -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
     -I $COQTOP/plugins/ring \
-    -I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
+    -I $COQTOP/plugins/rtauto \
     -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
     -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
     -I $COQTOP/ide \
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index 448e224f2e..74fcceb038 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -7,25 +7,7 @@ set -e
 
 dev/tools/check-overlays.sh
 
-# Can we check and fix formatting?
-# NB: we will ignore errors from ocamlformat as it fails when
-# encountering OCaml syntax errors
-ocamlformat=$(command -v ocamlformat || echo true)
-if [ "$ocamlformat" = true ]
-then
-    1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting."
-fi
-
-# Verify that the version of ocamlformat matches the one in .ocamlformat
-# The following command will print an error message if that's not the case
-# (and will print nothing if the versions match)
-if ! echo "let () = ()" | "$ocamlformat" --impl - > /dev/null
-then
-    1>&2 echo "Warning: Cannot check formatting."
-    ocamlformat=true
-fi
-
-1>&2 echo "Auto fixing whitespace and formatting issues..."
+1>&2 echo "Auto fixing whitespace issues..."
 
 # We fix whitespace in the index and in the working tree
 # separately to preserve non-added changes.
@@ -52,7 +34,6 @@ if [ -s "$index" ]; then
     git apply --cached --whitespace=fix "$index"
     git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
     git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-    { git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     git add -u
     1>&2 echo #newline
 fi
@@ -68,12 +49,11 @@ if [ -s "$tree" ]; then
     1>&2 echo "Fixing unstaged changes..."
     git apply --whitespace=fix "$tree"
     git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-    { git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     1>&2 echo #newline
 fi
 
 if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then
-    1>&2 echo "Fixing whitespace and formatting issues cancelled all changes."
+    1>&2 echo "Fixing whitespace issues cancelled all changes."
     exit 1
 fi
 
@@ -84,7 +64,7 @@ if ! git diff-index --check --cached HEAD; then
     1>&2 echo "(Consider whether the number of errors decreases after each run.)"
     exit 1
 fi
-1>&2 echo "Whitespace and formatting pass complete."
+1>&2 echo "Whitespace pass complete."
 
 # clean up temporary files
 rm "$index" "$tree" "$fixed_index"