17 files changed, 109 insertions, 46 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 9e9e3b4cfa..60c266699c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -97,11 +97,8 @@
 ########################################################################
 # Coquelicot
 ########################################################################
-# Modified until https://gitlab.inria.fr/coquelicot/coquelicot/merge_requests/2 is merged
-: "${coquelicot_CI_REF:=fix-rlist-import}"
-: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/pedrot/coquelicot}"
-# : "${coquelicot_CI_REF:=master}"
-# : "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
+: "${coquelicot_CI_REF:=master}"
+: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
 : "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
 
 ########################################################################
@@ -168,13 +165,6 @@
 : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}"
 
 ########################################################################
-# fiat_crypto_legacy
-########################################################################
-: "${fiat_crypto_legacy_CI_REF:=sp2019latest}"
-: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}"
-: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}"
-
-########################################################################
 # coq_dpdgraph
 ########################################################################
 : "${coq_dpdgraph_CI_REF:=coq-master}"
@@ -259,6 +249,13 @@
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
 
 ########################################################################
+# reduction-effects
+########################################################################
+: "${reduction_effects_CI_REF:=master}"
+: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}"
+: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}"
+
+########################################################################
 # menhirlib
 ########################################################################
 : "${menhirlib_CI_REF:=master}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
deleted file mode 100755
index 2af4b58201..0000000000
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-FORCE_GIT=1
-git_download fiat_crypto_legacy
-
-fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
-fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
-
-( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
-  ./etc/ci/remove_autogenerated.sh && \
-  make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 000c418137..811fefda35 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,11 +9,15 @@ git_download fiat_crypto
 # We need a larger stack size to not overflow ocamlopt+flambda when
 # building the executables.
 # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
+fiat_crypto_CI_STACKSIZE=32768
 
-fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1"
+# fiat-crypto is not guaranteed to build with the latest version of
+# bedrock2, so we use the pinned version of bedrock2, but the external
+# version of other developments
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
 fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
 fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
-        ulimit -s 32768 && \
+        ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
         make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh
index 7075d4d7f6..e08dcf07ab 100755
--- a/dev/ci/ci-mtac2.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -3,10 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download unicoq
-
-( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install )
-
 git_download mtac2
 
 ( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh
new file mode 100755
index 0000000000..6b6de3fa2f
--- /dev/null
+++ b/dev/ci/ci-reduction_effects.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download reduction_effects
+
+( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install)
diff --git a/dev/ci/ci-unicoq.sh b/dev/ci/ci-unicoq.sh
new file mode 100755
index 0000000000..36acb115e9
--- /dev/null
+++ b/dev/ci/ci-unicoq.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download unicoq
+
+( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install )
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index f08a08531f..c8ea59f08a 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -91,7 +91,6 @@ let projects = {
   cross_crypto = callPackage ./cross_crypto.nix {};
   Elpi = callPackage ./Elpi.nix {};
   fiat_crypto = callPackage ./fiat_crypto.nix {};
-  fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {};
   flocq = callPackage ./flocq.nix {};
   formal-topology = callPackage ./formal-topology.nix {};
   GeoCoq = callPackage ./GeoCoq.nix {};
diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix
deleted file mode 100644
index 3248665579..0000000000
--- a/dev/ci/nix/fiat_crypto_legacy.nix
+++ /dev/null
@@ -1,6 +0,0 @@
-{}:
-
-{
-  configure = "./etc/ci/remove_autogenerated.sh";
-  make = "make print-old-pipeline-lite old-pipeline-lite lite-display";
-}
diff --git a/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh
new file mode 100644
index 0000000000..87dad61dbc
--- /dev/null
+++ b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10204" ] || [ "$CI_BRANCH" = "rm-unsafe-type-of-coercion" ]; then
+
+    paramcoq_CI_REF=fix-papp
+    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
new file mode 100644
index 0000000000..fd63980036
--- /dev/null
+++ b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]; then
+
+    quickchick_CI_REF=non_maximal_implicit
+    quickchick_CI_GITURL=https://github.com/SimonBoulier/QuickChick
+
+    elpi_CI_REF=non_maximal_implicit
+    elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh
new file mode 100644
index 0000000000..5fb29e1826
--- /dev/null
+++ b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11417" ] || [ "$CI_BRANCH" = "rm-kind-of-type" ]; then
+
+    elpi_CI_REF=rm-kind-of-type
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh
new file mode 100644
index 0000000000..f2a431978d
--- /dev/null
+++ b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "11521" ] || [ "$CI_BRANCH" = "no-optname" ]; then
+
+    coqhammer_CI_REF=no-optname
+    coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer
+
+    equations_CI_REF=no-optname
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    unicoq_CI_REF=no-optname
+    unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq
+
+    paramcoq_CI_REF=no-optname
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh
new file mode 100644
index 0000000000..913b39c30c
--- /dev/null
+++ b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11557" ] || [ "$CI_BRANCH" = "template-directify" ]; then
+
+    equations_CI_REF=template-directify
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    paramcoq_CI_REF=template-directify
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+    elpi_CI_REF=template-directify
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md
index 3db5d0b14f..f81630c55d 100644
--- a/dev/doc/INSTALL.make.md
+++ b/dev/doc/INSTALL.make.md
@@ -102,6 +102,14 @@ Detailed Installation Procedure.
    it is recommended to compile in parallel, via make -jN where N is your number
    of cores.
 
+   If you wish to create timing logs for the standard library, you can
+   pass `TIMING=1` (for per-line timing files) or `TIMED=1` (for
+   per-file timing on stdout).  Further variables and targets are
+   available for more detailed timing analysis; see the section of the
+   reference manual on `coq_makefile`.  If there is any timing target
+   or variable supported by `coq_makefile`-made Makefiles which is not
+   supported by Coq's own Makefile, please report that as a bug.
+
 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
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 04b20c6889..cb6e695865 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,13 @@
 
 ### ML API
 
+Exception handling:
+
+- Coq's custom `Backtrace` module has been removed in favor of OCaml's
+  native backtrace implementation. Please use the functions in
+  `Exninfo.capture` and `iraise` when re-raising inside an exception
+  handler.
+
 Printers:
 
 - Functions such as Printer.pr_lconstr_goal_style_env have been
@@ -10,6 +17,11 @@ Printers:
   Constrextern.extern_constr which were taking a boolean argument for
   the goal style now take instead a label.
 
+Implicit arguments:
+
+- The type `Impargs.implicit_kind` was removed in favor of
+  `Glob_term.binding_kind`.
+
 ## Changes between Coq 8.10 and Coq 8.11
 
 ### ML API
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index ba68501e04..58c2fcc68a 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -127,11 +127,11 @@ in time.
 - [ ] Send an e-mail on Coqdev announcing that the tag has been put so that
   package managers can start preparing package updates (including a
   `coq-bignums` compatible version).
-- [ ] Ping **@erikmd** to update the Docker images in `coqorg/coq`
-  (requires `coq-bignums` in `extra-dev` for a beta / in `released`
-  for a final release).
+- [ ] When opening the corresponding PR for `coq` in the opam repository ([`coq/opam-coq-archive`](https://github.com/coq/opam-coq-archive) or [`ocaml/opam-repository`](https://github.com/ocaml/opam-repository)),
+  the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq)
+  (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built).
 - [ ] Draft a release on GitHub.
-- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and
+- [ ] Get `@maximedenes` to sign the Windows and MacOS packages and
   upload them on GitHub.
 - [ ] Prepare a page of news on the website with the link to the GitHub release
   (see [coq/www#63](https://github.com/coq/www/pull/63)).
@@ -139,8 +139,6 @@ in time.
   *TODO: setup some continuous deployment for this.*
 - [ ] Merge the website update, publish the release
   and send announcement e-mails.
-- [ ] Ping **@Zimmi48** to publish a new version on Zenodo.
-  *TODO: automate this.*
 - [ ] Close the milestone
 
 ## At the final release time ##
@@ -160,7 +158,10 @@ in time.
 
 Repeat the generic process documented above for all releases.
 
+Ping `@Zimmi48` to:
+
 - [ ] Switch the default version of the reference manual on the website.
+- [ ] Publish a new version on Zenodo.
 
 ## At the patch-level release time ##
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 835c20a4f7..f640a33773 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -254,7 +254,9 @@ let ppenvwithcst e = pp
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
-let ppobj obj = Format.print_string (Libobject.object_tag obj)
+let ppobj obj =
+  let Libobject.Dyn.Dyn (tag, _) = obj in
+  Format.print_string (Libobject.Dyn.repr tag)
 
 let cnt = ref 0