15 files changed, 348 insertions, 108 deletions
diff --git a/dev/base_include b/dev/base_include
index 4841db8953..96a867475d 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -60,11 +60,11 @@ open Cases
 open Pattern
 open Patternops
 open Cbv
-open Classops
+open Coercionops
 open Arguments_renaming
 open Pretyping
 open Cbv
-open Classops
+open Coercionops
 open Clenv
 open Clenvtac
 open Constr_matching
@@ -134,7 +134,7 @@ open Tacticals
 open Tactics
 open Eqschemes
 
-open Class
+open ComCoercion
 open ComDefinition
 open Indschemes
 open Ind_tables
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 82cc7a7117..859b3e3166 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -921,69 +921,6 @@ function make_gtk_sourceview3 {
   build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/3.24  gtksourceview-3.24.11  tar.xz  make_arch_pkg_config
 }
 
-##### FLEXDLL FLEXLINK #####
-
-# Note: there is a circular dependency between flexlink and ocaml (resolved in Ocaml 4.03.)
-# For MinGW it is not even possible to first build an Ocaml without flexlink support,
-# Because Makefile.nt doesn't support this. So we have to use a binary flexlink.
-# One could of cause do a bootstrap run ...
-
-# Install flexdll objects
-
-function install_flexdll {
-  cp flexdll.h "$PREFIXMINGW/include"
-  if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
-    cp flexdll*_mingw.o "/usr/$TARGET_ARCH/bin"
-    cp flexdll*_mingw.o "$PREFIXOCAML/bin"
-  elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
-    cp flexdll*_mingw64.o "/usr/$TARGET_ARCH/bin"
-    cp flexdll*_mingw64.o "$PREFIXOCAML/bin"
-  else
-    echo "Unknown target architecture"
-    return 1
-  fi
-}
-
-# Install flexlink
-
-function install_flexlink {
-  cp flexlink.exe "/usr/$TARGET_ARCH/bin"
-
-  cp flexlink.exe "$PREFIXOCAML/bin"
-}
-
-# Get binary flexdll flexlink for building OCaml
-# An alternative is to first build an OCaml without shared library support and build flexlink with it
-
-function get_flex_dll_link_bin {
-  if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip 1 ; then
-    install_flexdll
-    install_flexlink
-    build_post
-  fi
-}
-
-# Build flexdll and flexlink from sources after building OCaml
-
-function make_flex_dll_link {
-  if build_prep https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 ; then
-    if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
-      # shellcheck disable=SC2086
-      log1 make $MAKE_OPT build_mingw flexlink.exe
-    elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
-      # shellcheck disable=SC2086
-      log1 make $MAKE_OPT build_mingw64 flexlink.exe
-    else
-      echo "Unknown target architecture"
-      return 1
-    fi
-    install_flexdll
-    install_flexlink
-    log2 make clean
-    build_post
-  fi
-}
-
 ##### LN replacement #####
 
 # Note: this does support symlinks, but symlinks require special user rights on Windows.
@@ -1016,39 +953,22 @@ function make_arch_pkg_config {
 ##### OCAML #####
 
 function make_ocaml {
-  get_flex_dll_link_bin
-  if build_prep https://github.com/ocaml/ocaml/archive 4.07.1 tar.gz 1 ocaml-4.07.1 ; then
-    # See README.win32.adoc
-    cp config/m-nt.h byterun/caml/m.h
-    cp config/s-nt.h byterun/caml/s.h
-    if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
-        cp config/Makefile.mingw config/Makefile
-    elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
-        cp config/Makefile.mingw64 config/Makefile
-    else
-        echo "Unknown target architecture"
-        return 1
-    fi
+  if build_prep https://github.com/ocaml/ocaml/archive 4.08.1 tar.gz 1 ocaml-4.08.1 ; then
+    # see https://github.com/ocaml/ocaml/blob/4.08/README.win32.adoc
 
-    # Prefix is fixed in make file - replace it with the real one
-    # TODO: this might not work if PREFIX contains spaces
-    sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile
+    # get flexdll sources into folder ./flexdll
+    get_expand_source_tar https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 flexdll
 
     # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder
-    # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path:
-    # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
-    # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
-    # So we put an explicit path in there
-    sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile
-
-    # Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT
-    # I verified that 4.02.3 still doesn't support parallel build
-    log2 make world -f Makefile.nt
-    log2 make bootstrap -f Makefile.nt
-    log2 make opt -f Makefile.nt
-    log2 make opt.opt -f Makefile.nt
-    log2 make install -f Makefile.nt
-    # TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development
+    logn configure ./configure --build=i686-pc-cygwin --host="$TARGET_ARCH" --prefix="$PREFIXOCAML" --libdir="$PREFIXOCAML/libocaml"
+
+    log2 make flexdll $MAKE_OPT
+    # Note the next command might change after 4.09.x to just make
+    # see        https://github.com/ocaml/ocaml/blob/4.09/README.win32.adoc
+    # compare to https://github.com/ocaml/ocaml/blob/4.10/README.win32.adoc
+    log2 make world.opt $MAKE_OPT
+    log2 make flexlink.opt $MAKE_OPT
+    log2 make install $MAKE_OPT
 
     # Move license files and other into into special folder
     if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
@@ -1065,7 +985,6 @@ function make_ocaml {
 
     build_post
   fi
-  make_flex_dll_link
 }
 
 ##### OCAML EXTRA TOOLS #####
@@ -1099,7 +1018,7 @@ function make_num {
 
 function make_ocamlbuild {
   make_ocaml
-  if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then
+  if build_prep https://github.com/ocaml/ocamlbuild/archive 0.14.0 tar.gz 1 ocamlbuild-0.14.0; then
     log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib
     log1 make $MAKE_OPT
     log2 make install
@@ -1112,6 +1031,7 @@ function make_ocamlbuild {
 function make_findlib {
   make_ocaml
   make_ocamlbuild
+  # Note: latest is 1.8.1 but http://projects.camlcity.org/projects/dl/findlib-1.8.1/doc/README says this is for OCaml 4.09
   if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then
     logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf"
     # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
@@ -1385,7 +1305,7 @@ function copy_coq_license {
     # FIXME: this is not the micromega license
     # It only applies to code that was copied into one single file!
     install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
-    install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
+    install -D INSTALL.md                     "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
 }
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index b58a794da2..871d033f5b 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,5 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download equations
 
-( cd "${CI_BUILD_DIR}/equations" && coq_makefile -f _CoqProject -o Makefile && \
-  make && make test-suite && make examples && make install)
+( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci)
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8907843b12..b8f9d99702 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-12-03-V81"
+# CACHEKEY: "bionic_coq-V2019-12-08-V82"
 # ^^ 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.4/opam-2.0.4-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 # EDGE switch
 ENV COMPILER_EDGE="4.09.0" \
     COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \
-    BASE_OPAM_EDGE="dune-release.1.3.3"
+    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12"
 
 # 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/11027-SkySkimmer-expose-comind-univ.sh b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh
new file mode 100644
index 0000000000..bb65beb043
--- /dev/null
+++ b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh
@@ -0,0 +1,19 @@
+if [ "$CI_PULL_REQUEST" = "11027" ] || [ "$CI_BRANCH" = "cleanup-comind-univ" ]; then
+
+    elpi_CI_REF=expose-comind-univ
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=expose-comind-univ
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    paramcoq_CI_REF=expose-comind-univ
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+    mtac2_CI_REF=expose-comind-univ
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+    rewriter_CI_REF=cleanup-comind-univ
+    rewriter_CI_GITURL=https://github.com/SkySkimmer/rewriter
+
+
+fi
diff --git a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh
new file mode 100644
index 0000000000..fb66217487
--- /dev/null
+++ b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11141" ] || [ "$CI_BRANCH" = "master+labelled-pr_lconstr-and-co" ]; then
+
+    quickchick_CI_REF=master+adapt-coq-pr11141
+    quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
new file mode 100644
index 0000000000..a95170a455
--- /dev/null
+++ b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then
+
+    elpi_CI_REF=rename-class-files
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    mtac2_CI_REF=rename-class-files
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md
new file mode 100644
index 0000000000..3db5d0b14f
--- /dev/null
+++ b/dev/doc/INSTALL.make.md
@@ -0,0 +1,258 @@
+Quick Installation Procedure using Make.
+----------------------------------------
+
+    $ ./configure
+    $ make
+    $ make install (you may need superuser rights)
+
+Detailed Installation Procedure.
+--------------------------------
+
+1. Check that you have the OCaml compiler installed on your
+   computer and that `ocamlc` (or, better, its native code version
+   `ocamlc.opt`) is in a directory which is present in your $PATH
+   environment variable. At the time of writing this document, all
+   versions of Objective Caml later or equal to 4.05.0 are
+   supported.
+
+   To get Coq in native-code, (which runs 4 to 10 times faster than
+   bytecode, but it takes more time to get compiled and the binary is
+   bigger), you will also need the `ocamlopt` (or its native code version
+   `ocamlopt.opt`) command.
+
+2. The uncompression and un-tarring of the distribution file gave birth
+   to a directory named "coq-8.xx". You can rename this directory and put
+   it wherever you want. Just keep in mind that you will need some spare
+   space during the compilation (reckon on about 300 Mb of disk space
+   for the whole system in native-code compilation). Once installed, the
+   binaries take about 30 Mb, and the library about 200 Mb.
+
+3. First you need to configure the system. It is done automatically with
+   the command:
+
+        ./configure <options>
+
+   The `configure` script will ask you for directories where to put
+   the Coq binaries, standard library, man pages, etc. It will propose
+   default values.
+
+   For a list of options accepted by the `configure` script, run
+   `./configure -help`. The main options accepted are:
+
+   * `-prefix <dir>`
+     Binaries, library, and man pages will be respectively
+     installed in `<dir>/bin`, `<dir>/lib/coq`, and `<dir>/man`
+
+   * `-bindir <dir>`                   (default: `/usr/local/bin`)
+     Directory where the binaries will be installed
+
+   * `-libdir <dir>`                   (default: `/usr/local/lib/coq`)
+     Directory where the Coq standard library will be installed
+
+   * `-mandir <dir>`                   (default: `/usr/local/share/man`)
+     Directory where the Coq manual pages will be installed
+
+   * `-arch <value>`                   (default is the result of the command `arch`)
+     An arbitrary architecture name for your machine (useful when
+     compiling Coq on two different architectures for which the
+     result of "arch" is the same, e.g. Sun OS and Solaris)
+
+   * `-local`
+     Compile Coq to run in its source directory. The installation (step 6)
+     is not necessary in that case.
+
+   * `-browser <command>`
+     Use <command> to open an URL in a browser. %s must appear in <command>,
+     and will be replaced by the URL.
+
+   * `-flambda-opts <flags>`
+     This experimental option will pass specific user flags to the
+     OCaml optimizing compiler. In most cases, this option is used
+     to tweak the flambda backend; for maximum performance we
+     recommend using:
+
+         -flambda-opts `-O3 -unbox-closures`
+
+     but of course you are free to try with a different combination
+     of flags. You can read more at
+     https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html
+
+     There is a known problem with certain OCaml versions and
+     `native_compute`, that will make compilation to require
+     a large amount of RAM (>= 10GiB) in some particular files.
+
+     We recommend disabling native compilation (`-native-compiler no`)
+     with flambda unless you use OCaml >= 4.07.0.
+
+     c.f. https://caml.inria.fr/mantis/view.php?id=7630
+
+   If you want your build to be reproducible, ensure that the
+   SOURCE_DATE_EPOCH environment variable is set as documented in
+   https://reproducible-builds.org/specs/source-date-epoch/
+
+4. Still in the root directory, do
+
+        make
+
+   to compile Coq in the best OCaml mode available (native-code if supported,
+   bytecode otherwise).
+
+   This will compile the entire system. This phase can take more or less time,
+   depending on your architecture and is fairly verbose. On a multi-core machine,
+   it is recommended to compile in parallel, via make -jN where N is your number
+   of cores.
+
+5. You can now install the Coq system. Executables, libraries, and
+   manual pages are copied in some standard places of your system,
+   defined at configuration time (step 3). Just do
+
+        umask 022
+        make install
+
+   Of course, you may need superuser rights to do that.
+
+6. Optionally, you could build the bytecode version of Coq via:
+
+        make byte
+
+   and install it via
+
+        make install-byte
+
+  This version is much slower than the native code version of Coq, but could
+  be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
+  toplevel accessible via the Drop command.
+
+7. You can now clean all the sources. (You can even erase them.)
+
+        make clean
+
+Installation Procedure For Plugin Developers.
+---------------------------------------------
+
+If you wish to write plugins you *must* keep the Coq sources, without
+cleaning them. Therefore, to avoid a duplication of binaries and library,
+it is not necessary to do the installation step (6- above).  You just have
+to tell it at configuration step (4- above) with the option -local :
+
+    ./configure -local <other options>
+
+Then compile the sources as described in step 5 above. The resulting
+binaries will reside in the subdirectory bin/.
+
+Unless you pass the -nodebug option to ./configure, the -g option of the
+OCaml compiler will be used during compilation to allow debugging.
+See the debugging file in dev/doc and the chapter 15 of the Coq Reference
+Manual for details about how to use the OCaml debugger with Coq.
+
+
+The Available Commands.
+-----------------------
+
+There are two Coq commands:
+
+    coqtop          The Coq toplevel
+    coqc            The Coq compiler
+
+Under architecture where ocamlopt is available, coqtop is the native code
+version of Coq. On such architecture, you could additionally request
+the build of the bytecode version of Coq via 'make byte' and install it via
+'make install-byte'. This will create  an extra binary named coqtop.byte,
+that could be used for debugging purpose. If native code isn't available,
+coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
+coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
+and coqc selects a particular binary.
+
+* `coqtop` launches Coq in the interactive mode. By default it loads
+  basic logical definitions and tactics from the Init directory.
+
+* `coqc` allows compilation of Coq files directly from the command line.
+  To compile a file foo.v, do:
+
+        coqc foo.v
+
+  It will produce a file `foo.vo`, that you can now load through the Coq
+  command `Require`.
+
+  A detailed description of these commands and of their options is given
+  in the Reference Manual (which you can get in the doc/
+  directory, or read online on http://coq.inria.fr/doc/)
+  and in the corresponding manual pages.
+
+Compiling For Different Architectures.
+--------------------------------------
+
+This section explains how to compile Coq for several architecture, sharing
+the same sources. The important fact is that some files are architecture
+dependent (`.cmx`, `.o` and executable files for instance) but others are not
+(`.cmo` and `.vo`). Consequently, you can :
+
+-  save some time during compilation by not cleaning the architecture
+   independent files;
+
+-  save some space during installation by sharing the Coq standard
+   library (which is fully architecture independent).
+
+So, in order to compile Coq for a new architecture, proceed as follows:
+
+* Omit step 7 above and clean only the architecture dependent files:
+  it is done automatically with the command
+
+        make archclean
+
+* Configure the system for the new architecture:
+
+        ./configure <options>
+
+  You can specify the same directory for the standard library but you
+  MUST specify a different directory for the binaries (of course).
+
+* Compile and install the system as described in steps 5 and 6 above.
+
+Moving Binaries Or Library.
+---------------------------
+
+If you move both the binaries and the library in a consistent way,
+Coq should be able to still run. Otherwise, Coq may be "lost",
+running "coqtop" would then return an error message of the kind:
+
+    Error during initialization :
+    Error: cannot guess a path for Coq libraries; please use -coqlib option
+
+You can then indicate the new places to Coq, using the options -coqlib :
+
+    coqtop -coqlib <new directory>
+
+See also next section.
+
+Dynamically Loaded Libraries For Bytecode Executables.
+------------------------------------------------------
+
+Some bytecode executables of Coq use the OCaml runtime, which dynamically
+loads a shared library (.so or .dll). When it is not installed properly, you
+can get an error message of this kind:
+
+    Fatal error: cannot load shared library dllcoqrun
+    Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
+
+In this case, you need either:
+
+- to set the `CAML_LD_LIBRARY_PATH` environment variable to point to the
+  directory where dllcoqrun.so is; this is suitable when you want to run
+  the command a limited number of times in a controlled environment (e.g.
+  during compilation of binary packages);
+- install dllcoqrun.so in a location listed in the file ld.conf that is in
+  the directory of the standard library of OCaml;
+- recompile your bytecode executables after reconfiguring the location
+  of the shared library:
+
+        ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
+
+  where `<path>` is the directory where the dllcoqrun.so is installed;
+- (not recommended) compile bytecode executables with a custom OCaml
+  runtime by using:
+
+        ./configure -custom ...
+
+  be aware that stripping executables generated this way, or performing
+  other executable-specific operations, will make them useless.
diff --git a/dev/doc/README.md b/dev/doc/README.md
index bc281e0d94..ba53605b0e 100644
--- a/dev/doc/README.md
+++ b/dev/doc/README.md
@@ -43,8 +43,12 @@ To learn how to run the test suite, you can read
 
 
 ## Development environment + tooling
+
 - [`Merlin`](https://github.com/ocaml/merlin) for autocomplete.
 - [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup)
+- [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) provides
+  support for automatic formatting of OCaml code. To use it please run
+  `dune build @fmt`, see `ocamlformat`'s documentation for more help.
 
 ## A note about rlwrap
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 7d394c3401..04b20c6889 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,15 @@
 ## Changes between Coq 8.11 and Coq 8.12
 
+### ML API
+
+Printers:
+
+- Functions such as Printer.pr_lconstr_goal_style_env have been
+  removed, use instead functions such as pr_lconstr with label
+  `goal_concl_style:true`. Functions such as
+  Constrextern.extern_constr which were taking a boolean argument for
+  the goal style now take instead a label.
+
 ## Changes between Coq 8.10 and Coq 8.11
 
 ### ML API
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 67becb251a..2d187f7bae 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -255,6 +255,18 @@ Conversion machines
   GH issue number: #9925
   risk:
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: broken long multiplication primitive integer emulation layer on 32 bits
+  introduced: e43b176
+  impacted released versions: 8.10.0, 8.10.1, 8.10.2
+  impacted development branches: 8.11
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 4e176a7
+  found by: Soegtrop, Melquiond
+  exploit: test-suite/bugs/closed/bug_11321.v
+  GH issue number: #11321
+  risk: critical, as any BigN computation on 32-bit architectures is wrong
+
   component: "native" conversion machine (translation to OCaml which compiles to native code)
   summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
   introduced: V8.5
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 2e8a7455de..224601bbce 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -32,4 +32,7 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 |
 echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
+echo Checking ocamlformat
+dune build @fmt || CODE=1
+
 exit $CODE
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index e7a0ba4f6c..677377f868 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/4cd2cb43fb3a87f48c1e10bb65aee99d8f24cb9d.tar.gz";
-  sha256 = "1d6rmq67kdg5gmk94wx2774qw89nvbhy6g1f2lms3c9ph37hways";
+  url = "https://github.com/NixOS/nixpkgs/archive/f4ad230f90ef312695adc26f256036203e9c70af.tar.gz";
+  sha256 = "0cdd275dz3q51sknn7s087js81zvaj5riz8f29id6j6chnyikzjq";
 })
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f7f2bcdcff..835c20a4f7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -47,7 +47,7 @@ let ppmind kn = pp(MutInd.debug_print kn)
 let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
 let ppsp sp = pp(pr_path sp)
 let ppqualid qid = pp(pr_qualid qid)
-let ppclindex cl = pp(Classops.pr_cl_index cl)
+let ppclindex cl = pp(Coercionops.pr_cl_index cl)
 let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
 
 let prrecarg = function
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 5a2144f996..133326523b 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -29,7 +29,7 @@ val ppind : Names.inductive -> unit
 val ppsp : Libnames.full_path -> unit
 val ppqualid : Libnames.qualid -> unit
 
-val ppclindex : Classops.cl_index -> unit
+val ppclindex : Coercionops.cl_index -> unit
 
 val ppscheme : 'a Ind_tables.scheme_kind -> unit