23 files changed, 97 insertions, 51 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index cde1d798a0..fcc585117b 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1026,7 +1026,7 @@ function make_num {
 
 function make_zarith {
   make_ocaml
-  if build_prep https://github.com/ocaml/Zarith/archive release-1.9.1 tar.gz 1 zarith-1.9.1; then
+  if build_prep https://github.com/ocaml/Zarith/archive release-1.10 tar.gz 1 zarith-1.10; then
     logn configure ./configure
     log1 make
     log2 make install
diff --git a/dev/build/windows/patches_coq/ocaml-4.08.1.patch b/dev/build/windows/patches_coq/ocaml-4.08.1.patch
new file mode 100644
index 0000000000..a79033a061
--- /dev/null
+++ b/dev/build/windows/patches_coq/ocaml-4.08.1.patch
@@ -0,0 +1,25 @@
+diff --git a/runtime/caml/misc.h b/runtime/caml/misc.h
+index 6aa98516b..8184c2797 100644
+--- a/runtime/caml/misc.h
++++ b/runtime/caml/misc.h
+@@ -327,7 +327,6 @@ extern void caml_set_fields (intnat v, uintnat, uintnat);
+ 
+ #if defined(_WIN32) && !defined(_UCRT)
+ extern int caml_snprintf(char * buf, size_t size, const char * format, ...);
+-#define snprintf caml_snprintf
+ #endif
+ 
+ #ifdef CAML_INSTR
+@@ -336,6 +335,12 @@ extern int caml_snprintf(char * buf, size_t size, const char * format, ...);
+ #include <time.h>
+ #include <stdio.h>
+ 
++/* snprintf emulation for Win32 - do define after stdio.h, in case snprintf is defined */
++
++#if defined(_WIN32) && !defined(_UCRT)
++#define snprintf caml_snprintf
++#endif
++
+ extern intnat caml_stat_minor_collections;
+ extern intnat caml_instr_starttime, caml_instr_stoptime;
+ 
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 17d71ac52a..f2397cdcee 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.10.0+mingw64c
+OPAM_VARIANT=ocaml-variants.4.11.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-common.sh b/dev/ci/ci-common.sh
index c01bc57f72..f9187d53a6 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -97,9 +97,9 @@ make()
     if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ];
     then
         # Not submake and parallel make requested
-        command make -j "$NJOBS" "$@"
+        command make --output-sync -j "$NJOBS" "$@"
     else
-        command make "$@"
+        command make --output-sync "$@"
     fi
 }
 
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/ci-mathcomp.sh b/dev/ci/ci-mathcomp.sh
index cae127ee7b..b1aa56ec4e 100755
--- a/dev/ci/ci-mathcomp.sh
+++ b/dev/ci/ci-mathcomp.sh
@@ -6,7 +6,7 @@ ci_dir="$(dirname "$0")"
 
 git_download mathcomp
 
-( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install )
+( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make test-suite && make install )
 
 git_download fourcolor
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 78c8673299..f672ead807 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-08-28-V92"
+# CACHEKEY: "bionic_coq-V2020-09-17-V88"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -40,10 +40,8 @@ ENV NJOBS="2" \
 # Base opam is the set of base packages required by Coq
 ENV COMPILER="4.05.0"
 
-# Common OPAM packages, num to be removed once the migration to
-# micromega is complete, `num` also does not have a version number as
-# the right version to install varies with the compiler version.
-ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.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"
 
@@ -59,12 +57,12 @@ RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opa
 
 # base+32bit switch, note the zarith hack
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
-        i386 env CC='gcc -m32' opam install zarith.1.9.1 && \
+        i386 env CC='gcc -m32' opam install zarith.1.10 && \
         opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.10.0" \
-    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.14.2"
+ENV COMPILER_EDGE="4.11.1" \
+    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.15.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 05624ff4a1..7863af842a 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -114,6 +114,7 @@ let projects = {
   mtac2 = callPackage ./mtac2.nix {};
   oddorder = callPackage ./oddorder.nix {};
   quickchick = callPackage ./quickchick.nix {};
+  simple-io = callPackage ./simple-io.nix {};
   verdi-raft = callPackage ./verdi-raft.nix {};
   VST = callPackage ./VST.nix {};
 }; in
@@ -130,7 +131,8 @@ stdenv.mkDerivation {
   name = "shell-for-${project}-in-${branch}";
 
   buildInputs =
-    optional withCoq coq
+    [ python ]
+  ++  optional withCoq coq
   ++ (prj.buildInputs or [])
   ++ optionals withCoq (prj.coqBuildInputs or [])
   ;
diff --git a/dev/ci/nix/simple-io.nix b/dev/ci/nix/simple-io.nix
new file mode 100644
index 0000000000..3b7b6c09b1
--- /dev/null
+++ b/dev/ci/nix/simple-io.nix
@@ -0,0 +1,5 @@
+{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }:
+{
+  buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ];
+  coqBuildInputs = [ ssreflect coq-ext-lib ];
+}
diff --git a/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh b/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh
new file mode 100644
index 0000000000..7bed43afe1
--- /dev/null
+++ b/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12977" ] || [ "$CI_BRANCH" = "static-hint-poly" ]; then
+
+    equations_CI_REF=static-hint-poly
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    fiat_parsers_CI_REF=static-hint-poly
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
+
+fi
diff --git a/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh b/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh
new file mode 100644
index 0000000000..3407c2db39
--- /dev/null
+++ b/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13028" ] || [ "$CI_BRANCH" = "master+fix-quotations-printing" ]; then
+
+    equations_CI_REF=master+adapt-coq-pr13028-quotation-qualifier-printing
+    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+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/doc/changes.md b/dev/doc/changes.md
index ae4c6328b5..59c1623a2d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,15 @@
 ## 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.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
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/dune-workspace.all b/dev/dune-workspace.all
index d6348a3624..679b3d1f79 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.10.0)))
-(context (opam (switch 4.10.0+flambda)))
+(context (opam (switch 4.11.1)))
+(context (opam (switch 4.11.1+flambda)))
diff --git a/dev/include_printers b/dev/include_printers
index 30529b5fd6..7583762970 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -26,6 +26,8 @@
 #install_printer  (* judgement *) ppj;;
 #install_printer  (* id set *) ppidset;;
 #install_printer  (* int set *) ppintset;;
+#install_printer  (* id set *) ppidmapgen;;
+#install_printer  (* int set *) ppintmapgen;;
 
 #install_printer  (* Reductionops machine stack *) pp_stack_t;;
 
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/nixpkgs.nix b/dev/nixpkgs.nix
index bfb25e72dd..a582a70e0a 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/17812e653d89c46d68b7b10e290b1c16758f4e47.tar.gz";
-  sha256 = "1zcb70dyfqc8l2ywpbvxmpfshapdi0g365m3rhmwpagqg47pnyxs";
+  url = "https://github.com/NixOS/nixpkgs/archive/0bbeca2ff952e6a171534793ddd0fa97c8f9546a.tar.gz";
+  sha256 = "0h1y4ffvyvkqs6k2pak02pby25va7c6c1y4p8xkwlzqwswxqxvfl";
 })
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"
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 60618f6491..21d6fbe9aa 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -28,6 +28,7 @@ install_printer Top_printers.ppnumtokunsignednat
 install_printer Top_printers.ppintset
 install_printer Top_printers.ppidset
 install_printer Top_printers.ppidmapgen
+install_printer Top_printers.ppintmapgen
 install_printer Top_printers.ppididmap
 install_printer Top_printers.ppconstrunderbindersidmap
 install_printer Top_printers.ppevarsubst
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 773170207e..e4dd7ef52c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -94,11 +94,13 @@ let pridmap pr l =
   prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
 let ppidmap pr l = pp (pridmap pr l)
 
-let pridmapgen l =
-  let dom = Id.Set.elements (Id.Map.domain l) in
+let prmapgen pr dom =
   if dom = [] then str "[]" else
-  str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]"
+  str "[domain= " ++ hov 0 (prlist_with_sep spc pr dom) ++ str "]"
+let pridmapgen l = prmapgen Id.print (Id.Set.elements (Id.Map.domain l))
 let ppidmapgen l = pp (pridmapgen l)
+let printmapgen l = prmapgen int (Int.Set.elements (Int.Map.domain l))
+let ppintmapgen l = pp (printmapgen l)
 
 let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
   hov 0
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index b1bb5e4702..712f66112c 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -65,6 +65,9 @@ val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit
 val pridmapgen : 'a Names.Id.Map.t -> Pp.t
 val ppidmapgen : 'a Names.Id.Map.t -> unit
 
+val printmapgen : 'a Int.Map.t -> Pp.t
+val ppintmapgen : 'a Int.Map.t -> unit
+
 val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t
 val ppididmap : Names.Id.t Names.Id.Map.t -> unit