23 files changed, 185 insertions, 378 deletions
diff --git a/dev/README.md b/dev/README.md
index 4642aaf06d..d9fdd230d3 100644
--- a/dev/README.md
+++ b/dev/README.md
@@ -34,9 +34,8 @@
 | [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release |
 
 
-## Documentation of ML interfaces using ocamldoc ( `dev/ocamldoc/html`)
-`make mli-doc` in coq root directory.
-
+## Documentation of ML interfaces using `odoc` ( `_build/default/_doc`)
+`make -f Makefile.dune apidoc` in coq root directory.
 
 ## Other development tools (`dev/tools`)
 
diff --git a/dev/base_include b/dev/base_include
index 6f54ecb241..67a7e87d78 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -99,7 +99,6 @@ open Evarutil
 open Evarsolve
 open Tacred
 open Evd
-open Universes
 open Termops
 open Namegen
 open Indrec
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 5f07aa8fca..c3d895784e 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1374,7 +1374,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 CHANGES                        "$PREFIXCOQ/license_readme/coq/Changes.txt"
+    install -D CHANGES.md                     "$PREFIXCOQ/license_readme/coq/Changes.md"
     install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
@@ -1851,7 +1851,7 @@ function make_addon_coquelicot {
 
 function make_addon_aactactics {
   installer_addon_dependency aac
-  if build_prep_overlay aactactis; then
+  if build_prep_overlay aactactics; then
     installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" ""
     log1 make
     log2 make install
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 3a179a9431..7853866f62 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project:
    developer who merges the PR on Coq. There are plans to improve this, cf.
    [#6724](https://github.com/coq/coq/issues/6724).
 
-Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
 
 Advanced GitLab CI information
 ------------------------------
@@ -167,10 +167,7 @@ Currently available artifacts are:
   + Coq's Standard Library Documentation [master branch]
     https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman
   + Coq's ML API Documentation [master branch]
-    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api:ocamldoc
-
-  The dune job also provides its own API documentation using the newer `odoc` tool:
-  https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
 
 ### GitLab and Windows
 
@@ -178,6 +175,11 @@ If your repository has access to runners tagged `windows`, setting the
 secret variable `WINDOWS` to `enabled` will add jobs building Windows
 versions of Coq (32bit and 64bit).
 
+If the secret variable `WINDOWS` is set to `enabled_all_addons`,
+an extended set of addons will be added to the Windows installer.
+This leads to a considerable runtime in CI so this is not enabled
+by default for pipelines for pull requests.
+
 The Windows jobs are enabled on Coq's repository, where pipelines for
 pull requests run.
 
diff --git a/dev/ci/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh
new file mode 100755
index 0000000000..896a0ddf66
--- /dev/null
+++ b/dev/ci/ci-aac-tactics.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download aactactics
+
+( cd "${CI_BUILD_DIR}/aactactics" && make && make install )
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 1b1aeafa0d..50d4d21637 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -49,11 +49,12 @@
 ########################################################################
 # Iris
 ########################################################################
-: "${stdpp_CI_REF:=master}"
+
+# NB: stdpp and Iris refs are gotten from the opam files in the Iris
+# and lambdaRust repos respectively.
 : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}"
 : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
 
-: "${Iris_CI_REF:=master}"
 : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}"
 : "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
 
@@ -251,6 +252,6 @@
 ########################################################################
 # aac-tactics
 ########################################################################
-: "${aactactis_CI_REF:=master}"
-: "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
-: "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}"
+: "${aactactics_CI_REF:=master}"
+: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
+: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index e0395754e5..6bf3138346 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -10,4 +10,5 @@ fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-d
 fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && 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-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index 6960a8b98a..95f143bb95 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -9,13 +9,13 @@ install_ssreflect
 git_download lambdaRust
 
 # Extract required version of Iris
-Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
+Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup Iris
 git_download Iris
 
 # Extract required version of std++
-stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
+stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([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 fcfa591ce1..f257c62dd3 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-09-25-V1"
+# CACHEKEY: "bionic_coq-V2018-10-04-V2"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV CAMLP5_VER="7.01" \
+ENV CAMLP5_VER="7.03" \
     COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
 # base switch
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index deda42e2b7..918d289ae2 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -37,8 +37,21 @@ SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
 SET COQREGTESTING=Y
 SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
 
-if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
-if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+IF "%WINDOWS%" == "enabled_all_addons" (
+  SET EXTRA_ADDONS=^
+    -addon=mathcomp ^
+    -addon=menhir ^
+    -addon=menhirlib ^
+    -addon=compcert ^
+    -addon=extlib ^
+    -addon=quickchick ^
+    -addon=coquelicot
+  REM addons with build issues
+  REM -addon=vst ^
+  REM -addon=aactactics ^
+) ELSE (
+  SET "EXTRA_ADDONS= "
+)
 
 call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
   -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
@@ -47,20 +60,10 @@ call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
   -addon=equations ^
   -addon=ltac2 ^
   -addon=mtac2 ^
-  -addon=mathcomp ^
-  -addon=menhir ^
-  -addon=menhirlib ^
-  -addon=compcert ^
-  -addon=extlib ^
-  -addon=quickchick ^
-  -addon=coquelicot ^
+  %EXTRA_ADDONS% ^
   -make=N ^
   -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
 
-REM addons with build issues
-REM -addon=vst ^
-REM -addon=aactactics ^
-
 ECHO "Start Artifact Creation"
 TIME /T
 
diff --git a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
new file mode 100644
index 0000000000..484ad8f9e6
--- /dev/null
+++ b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
@@ -0,0 +1,11 @@
+if [ "$CI_PULL_REQUEST" = "8554" ] || [ "$CI_BRANCH" = "master+fix8553-change-under-binders" ]; then
+
+    ltac2_CI_BRANCH=master+fix-pr8554-change-takes-env
+    ltac2_CI_REF=master+fix-pr8554-change-takes-env
+    ltac2_CI_GITURL=https://github.com/herbelin/ltac2
+
+    Equations_CI_BRANCH=master+fix-pr8554-change-takes-env
+    Equations_CI_REF=master+fix-pr8554-change-takes-env
+    Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
new file mode 100644
index 0000000000..41c2ad6fef
--- /dev/null
+++ b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then
+
+    ltac2_CI_REF=rm-section-path
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    Equations_CI_REF=rm-section-path
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index c0cd9c8cdd..000f21c254 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -54,7 +54,7 @@ those external projects should have been prepared (cf. the relevant sub-section
 in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
 with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
 
-Moreover the PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
 
 If overlays are missing, ask the author to prepare them and label the PR with
 the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
@@ -93,7 +93,7 @@ When the PR has conflicts, the assignee can either:
 
 In both cases, CI should be run again.
 
-In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix
 the conflicts in the merge commit (following the same steps as below), and push
 to `master` directly. Don't use the GitHub interface to fix these conflicts.
 
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 7349360be8..91ab57f1e9 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -107,6 +107,17 @@ global options --- such as flags --- on all packages, or build Coq
 with different OPAM switches simultaneously [for example to test
 compatibility]; for more information, please refer to the Dune manual.
 
+## Inlining reports
+
+The `ireport` profile will produce standard OCaml [inlining
+reports](https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html#sec488). These
+are to be found under `_build/default/$lib/$lib.objs/$module.$round.inlining.org`
+and are in Emacs `org-mode` format.
+
+Note that due to https://github.com/ocaml/dune/issues/1401 , we must
+perform a full rebuild each time as otherwise Dune will remove the
+files. We hope to solve this in the future.
+
 ## Documentation and test targets
 
 The documentation and test suite targets for Coq are still not
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fdeb0abed4..f30b4107b6 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,10 +2,30 @@
 
 ### ML API
 
-Termops:
+General deprecation
 
-- Internal printing functions have been placed under the
-  `Termops.Internal` namespace.
+- All functions marked [@@ocaml.deprecated] in 8.8 have been
+  removed. Please, make sure your plugin is warning-free in 8.8 before
+  trying to port it over 8.9.
+
+Names
+
+- Kernel names no longer contain a section path. They now have only two
+  components (module path and label), which led to some changes in the API:
+
+  KerName.make takes only 2 components
+  KerName.repr returns only 2 components
+  KerName.make2 is now KerName.make
+  Constant.make3 has been removed, use Constant.make2
+  Constant.repr3 has been removed, use Constant.repr2
+
+Coqlib:
+
+- Most functions from the `Coqlib` module have been deprecated in favor of
+  `register_ref` and `lib_ref`. The first one is available through the
+  vernacular `Register` command; it binds a name to a constant. The second
+  command then enables to locate the registered constant through its name. The
+  name resolution is dynamic.
 
 ## Changes between Coq 8.8 and Coq 8.9
 
@@ -16,8 +36,8 @@ Names
 - In `Libnames`, the type `reference` and its two constructors `Qualid` and
   `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity,
   `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be
-  replaced by a test using `qualid_is_ident`. Extracting the ident part of a
-  qualid can be done using `qualid_basename`.
+  replaced by a test using `qualid_is_ident`. Extracting the `ident` part of a
+  `qualid` can be done using `qualid_basename`.
 
 Misctypes
 
@@ -51,20 +71,20 @@ Proof engine
 
 ML Libraries used by Coq
 
-- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
-  Array.Smart.map.
-- Uniformization of some names, e.g. Array.Smart.fold_left_map instead
-  of Array.smartfoldmap.
+- Introduction of a `Smart` module for collecting `smart*` functions, e.g.
+  `Array.Smart.map`.
+- Uniformization of some names, e.g. `Array.Smart.fold_left_map` instead
+  of `Array.smartfoldmap`.
 
 Printer.ml API
 
-- The mechanism in Printer that allowed dynamically overriding pr_subgoals,
-  pr_subgoal and pr_goal was removed to simplify the code.  It was
-  earlierly used by PCoq.
+- The mechanism in `Printer` that allowed dynamically overriding `pr_subgoals`,
+  `pr_subgoal` and `pr_goal` was removed to simplify the code.  It was
+  earlier used by PCoq.
 
 Kernel
 
-  The following renamings happened:
+- The following renamings happened:
   - `Context.Rel.t` into `Constr.rel_context`
   - `Context.Named.t` into `Constr.named_context`
   - `Context.Compacted.t` into `Constr.compacted_context`
@@ -93,19 +113,24 @@ Vernacular commands
 
 Primitive number parsers
 
-- For better modularity, the primitive parsers for positive, N and Z
-  have been split over three files (plugins/syntax/positive_syntax.ml,
-  plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml).
+- For better modularity, the primitive parsers for `positive`, `N` and `Z`
+  have been split over three files (`plugins/syntax/positive_syntax.ml`,
+  `plugins/syntax/n_syntax.ml`, `plugins/syntax/z_syntax.ml`).
 
 Parsing
 
-- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules
-  Pcoq.Entry and Pcoq.Parsable were introduced to replace it.
+- Manual uses of the `Pcoq.Gram` module have been deprecated. Wrapper modules
+  `Pcoq.Entry` and `Pcoq.Parsable` were introduced to replace it.
+
+Termops
+
+- Internal printing functions have been placed under the
+  `Termops.Internal` namespace.
 
 ### Unit testing
 
-  The test suite now allows writing unit tests against OCaml code in the Coq
-  code base. Those unit tests create a dependency on the OUnit test framework.
+The test suite now allows writing unit tests against OCaml code in the Coq
+code base. Those unit tests create a dependency on the OUnit test framework.
 
 ### Transitioning away from Camlp5
 
@@ -140,7 +165,7 @@ let myval = 0
 
 Steps to perform:
 - replace the brackets enclosing OCaml code in actions with braces
-- if not there yet, add a leading `|̀  to the first rule
+- if not there yet, add a leading `|` to the first rule
 
 For instance, code of the form:
 ```
@@ -159,7 +184,28 @@ END
 
 #### VERNAC EXTEND
 
-Not handled yet.
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions and rule classifiers with
+  braces
+- if not there yet, add a leading `|̀  to the first rule
+
+Handwritten classifiers declared through the `CLASSIFIED BY` statement are
+considered OCaml code, so they also need to be wrapped in braces.
+
+For instance, code of the form:
+```
+VERNAC COMMAND EXTEND my_command CLASSIFIED BY classifier
+  [ "foo" int(i) ] => [ classif' ] -> [ cmd1 i ]
+| [ "bar" ] -> [ cmd2 ]
+END
+```
+should be turned into
+```
+VERNAC COMMAND EXTEND my_command CLASSIFIED BY { classifier }
+| [ "foo" int(i) ] => { classif' } -> { cmd1 i }
+| [ "bar" ] -> { cmd2 }
+END
+```
 
 #### ARGUMENT EXTEND
 
@@ -171,8 +217,8 @@ Most plugin writers do not need this low-level interface, but for the sake of
 completeness we document it.
 
 Steps to perform are:
-- replace GEXTEND with GRAMMAR EXTEND
-- wrap every occurrence of OCaml code in actions into braces { }
+- replace `GEXTEND` with `GRAMMAR EXTEND`
+- wrap every occurrence of OCaml code in actions into braces `{ }`
 
 For instance, code of the form
 ```
@@ -222,7 +268,7 @@ All the other bugs kept their number.
 
 General deprecation
 
-- All functions marked [@@ocaml.deprecated] in 8.7 have been
+- All functions marked `[@@ocaml.deprecated]` in 8.7 have been
   removed. Please, make sure your plugin is warning-free in 8.7 before
   trying to port it over 8.8.
 
@@ -250,8 +296,8 @@ We changed the type of the following functions:
 
 - `Global.body_of_constant`: same as above.
 
-- `Constrinterp.*` generally, many functions that used to take an
-  `evar_map ref` have been now switched to functions that will work in
+- `Constrinterp.*`: generally, many functions that used to take an
+  `evar_map ref` have now been switched to functions that will work in
   a functional way. The old style of passing `evar_map`s as references
   is not supported anymore.
 
@@ -269,16 +315,16 @@ We have changed the representation of the following types:
 
 Some tactics and related functions now support static configurability, e.g.:
 
-- injectable, dEq, etc. takes an argument ~keep_proofs which,
-  - if None, tells to behave as told with the flag Keep Proof Equalities
-  - if Some b, tells to keep proof equalities iff b is true
+- `injectable`, `dEq`, etc. take an argument `~keep_proofs` which,
+  - if `None`, tells to behave as told with the flag `Keep Proof Equalities`
+  - if `Some b`, tells to keep proof equalities iff `b` is true
 
 Declaration of printers for arguments used only in vernac command
 
-- It should now use "declare_extra_vernac_genarg_pprule" rather than
-  "declare_extra_genarg_pprule", otherwise, a failure at runtime might
+- It should now use `declare_extra_vernac_genarg_pprule` rather than
+  `declare_extra_genarg_pprule`, otherwise, a failure at runtime might
   happen. An alternative is to register the corresponding argument as
-  a value, using "Geninterp.register_val0 wit None".
+  a value, using `Geninterp.register_val0 wit None`.
 
 Types Alias deprecation and type relocation.
 
@@ -321,7 +367,7 @@ functions when some given constants are traversed:
 
   * `declare_reduction_effect`: to declare a hook to be applied when some
   constant are visited during the execution of some reduction functions
-  (primarily cbv).
+  (primarily `cbv`).
 
   * `set_reduction_effect`: to declare a constant on which a given effect
   hook should be called.
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 1a8a816aaa..93b807d5e3 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -1,10 +1,6 @@
 (lang dune 1.2)
 
 ; Add custom flags here. Default developer profile is `dev`
-(env
- (dev     (flags :standard -rectypes -w -9-27-50+60))
- (release (flags :standard -rectypes)))
-
 (context (opam (switch 4.05.0)))
 (context (opam (switch 4.05.0+32bit)))
 (context (opam (switch 4.07.0)))
diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro
deleted file mode 100644
index 33d20fc818..0000000000
--- a/dev/ocamldoc/docintro
+++ /dev/null
@@ -1,49 +0,0 @@
-{!indexlist}
-
-This is Coq, a proof assistant for the Calculus of Inductive Constructions.
-This document describes the implementation of Coq.
-It has been automatically generated from the source of
-Coq using {{:http://caml.inria.fr/}ocamldoc}.
-The source files are organized in several directories ordered like that:
-
-{ol {- Utility libraries : lib
-
-describes the various utility libraries used in the code
-of Coq.}
-{- Kernel : kernel
-
-describes the Coq kernel, which is a type checker for the Calculus
-of Inductive Constructions.}
-{- Library : library
-
-describes the Coq library, which is made of two parts:
-- a general mechanism to keep a trace of all operations and of
-    the state of the system, with backtrack capabilities;
-- a global environment for the CCI, with functions to export and 
-    import compiled modules.
-
-}
-{- Pretyping : pretyping
-
-}
-{- Front abstract syntax of terms : interp
-
-describes the translation from Coq context-dependent
-front abstract syntax of terms {v constr_expr v} to and from the
-context-free, untyped, globalized form of constructions {v glob_constr v}.}
-{- Parsers and printers : parsing
-
-describes the implementation of the Coq parsers and printers.}
-{- Proof engine : proofs
-
-describes the Coq proof engine, which is also called
-the ``refiner'', since it provides a way to build terms by successive
-refining steps. Those steps are either primitive rules or higher-level
-tactics.}
-{- Tacticts : tactics
-
-describes the Coq main tactics.}
-{- Toplevel : toplevel
-
-describes the highest modules of the Coq system.}
-}
diff --git a/dev/ocamldoc/fix-ocamldoc-utf8 b/dev/ocamldoc/fix-ocamldoc-utf8
deleted file mode 100755
index fe2e0c1155..0000000000
--- a/dev/ocamldoc/fix-ocamldoc-utf8
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-# This reverts automatic translation of latin1 accentuated letters by ocamldoc
-# Usage: fix-ocamldoc-utf8 file
-
-sed -i -e 's/\\`a/\d224/g' -e "s/\\\^a/\d226/g" -e "s/\\\'e/\d233/g" -e 's/\\`e/\d232/g' -e "s/\\\^e/\d234/g" -e 's/\\\"e/\d235/g' -e "s/\\\^o/\d244/g" -e 's/\\\"o/\d246/g' -e "s/\\\^i/\d238/g" -e 's/\\\"i/\d239/g' -e 's/\\`u/\d249/g' -e "s/\\\^u/\d251/g" -e "s/\\\c{c}/\d231/g" $1
diff --git a/dev/ocamldoc/header.tex b/dev/ocamldoc/header.tex
deleted file mode 100644
index 4091f8144f..0000000000
--- a/dev/ocamldoc/header.tex
+++ /dev/null
@@ -1,14 +0,0 @@
-\documentclass[11pt]{article} 
-\usepackage[utf8x]{inputenc} 
-\usepackage[T1]{fontenc} 
-\usepackage{textcomp}
-\usepackage{tipa}
-\usepackage{textgreek}
-\usepackage{fullpage} 
-\usepackage{url} 
-\usepackage{ocamldoc}
-\title{Coq mlis documentation}
-\begin{document}
-\maketitle
-\tableofcontents
-\vspace{0.2cm}
diff --git a/dev/ocamldoc/html/style.css b/dev/ocamldoc/html/style.css
deleted file mode 100644
index c2c45b6297..0000000000
--- a/dev/ocamldoc/html/style.css
+++ /dev/null
@@ -1,220 +0,0 @@
-a:visited {
-  color: #416DFF; text-decoration: none; 
-}
-
-a:link {
-  color: #416DFF; text-decoration: none;
-}
-
-a:hover {
-  color: Red; text-decoration: none; background-color: #5FFF88
-}
-
-a:active {
-  color: Red; text-decoration: underline; 
-}
-
-.keyword {
-  font-weight: bold; color: Red 
-}
-
-.keywordsign {
-  color: #C04600 
-}
-
-.superscript {
-  font-size: 8 
-}
-
-.subscript {
-  font-size: 8 
-}
-
-.comment {
-  color: Green 
-}
-
-.constructor {
-  color: Blue 
-}
-
-.type {
-  color: #5C6585 
-}
-
-.string {
-  color: Maroon 
-}
-
-.warning {
-  color: Red; font-weight: bold 
-}
-
-.info {
-  margin-left: 3em; margin-right: 3em 
-}
-
-.param_info {
-  margin-top: 4px; margin-left: 3em; margin-right: 3em 
-}
-
-.code {
-  color: #465F91; 
-}
-
-h1 {
-  font-size: 20pt; text-align: center; 
-}
-
-h5, h6, div.h7, div.h8, div.h9 {
-  font-size: 20pt;
-  border: 1px solid #000000;
-  margin-top: 5px;
-  margin-bottom: 2px;
-  text-align: center;
-  padding: 2px;
-}
-
-h5 {
-  background-color: #90FDFF;
-}
-
-h6 {
-  background-color: #016699;
-  color: white;
-}
-
-div.h7 {
-  background-color: #E0FFFF;
-}
-
-div.h8 {
-  background-color: #F0FFFF;
-}
-
-div.h9 {
-  background-color: #FFFFFF;
-}
-
-.typetable, .indextable, .paramstable {
-  border-style: hidden;
-}
-
-.paramstable {
-  padding: 5pt 5pt;
-}
-
-body {
-  background-color: white;
-}
-
-tr {
-  background-color: white;
-}
-
-td.typefieldcomment {
-  background-color: #FFFFFF;
-  font-size: smaller;
-}
-
-pre {
-  margin-bottom: 4px;
-}
-
-div.sig_block {
-  margin-left: 2em;
-}
-
-
-h2 {
-  font-family: Arial, Helvetica, sans-serif;
-  font-size: 16pt;
-  font-weight: normal;
-  border-bottom: 1px solid #dadada;
-  border-top: 1px solid #dadada;
-  color: #101010;
-  background: #eeeeff;
-  margin: 25px 0px 10px 0px;
-  padding: 1px 1px 1px 1px;
-}
-
-h3 {
-  font-family: Arial, Helvetica, sans-serif;
-  font-size: 12pt;
-  color: #016699;
-  font-weight: bold;
-  padding: 15px 0 0 0ex;
-  margin: 5px 0 0 0;
-}
-
-h4 {
-  font-family: Arial, Helvetica, sans-serif;
-  font-size: 10pt;
-  color: #016699;
-  padding: 15px 0 0 0ex;
-  margin: 5px 0 0 0;
-}
-
-/* Here starts the overwrite of default rules to give a better look */
-
-body {
-  font-family: Calibri, Georgia, Garamond, Baskerville, serif;
-  font-size: 12pt;
-  background-color: white;
-}
-
-a:link, a {
-  color: #6895c3 !important;
-}
-
-a:hover {
-  color: #2F4459 !important;
-  background-color: white;
-}
-
-hr {
-  height: 1px;
-  color: #016699;
-  background-color: #016699;
-  border-width: 0;
-}
-
-h1, h1 a:link, h1 a:visited, h1 a {
-  font-family: Cambria, Georgia, Garamond, Baskerville, serif;
-  color: #016699;
-}
-
-.navbar {
-  float: left;
-}
-
-.navbar a, .navbar a:link, .navbar a:visited {
-  color: #016699;
-  font-family: Arial, Helvetica, sans-serif;
-  font-weight: bold;
-  font-size: 80%;
-}
-
-.keyword {
-  color: #c13939;
-}
-
-.constructor {
-  color: #3c8f7e;
-}
-
-pre, code {
-  font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace;
-  white-space: normal;
-  font-size: 9pt;
-  font-weight: bold;
-}
-
-.type br {
-  display: none;
-}
-
-.info {
-  margin-left: 1em;
-  font-size: 12pt;
-}
diff --git a/dev/tools/make_git_revision.sh b/dev/tools/make_git_revision.sh
new file mode 100755
index 0000000000..84982f89b9
--- /dev/null
+++ b/dev/tools/make_git_revision.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+if [ -x `which git` ] && [ -d .git ] || git rev-parse --git-dir > /dev/null 2>&1
+then
+    export LANG=C
+    GIT_BRANCH=$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p')
+    GIT_HOST=$(hostname)
+    GIT_PATH=$(pwd)
+    echo "${GIT_HOST}:${GIT_PATH},${GIT_BRANCH}"
+    echo $(git log -1 --pretty='format:%H')
+fi
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 7c8b9f025c..14094553a2 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -17,7 +17,7 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml')
 COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
 G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
-BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', '4798.v')
+BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
                          for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
 TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current')
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e15fd776b2..44d44ccc4b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -527,7 +527,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))]
+        (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))]
 
 let _ =
   try
@@ -543,7 +543,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))]
+        (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
@@ -552,23 +552,22 @@ open Libnames
 let encode_path ?loc prefix mpdir suffix id =
   let dir = match mpdir with
     | None -> []
-    | Some (mp,dir) ->
-	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
-	DirPath.repr dir) in
+    | Some mp -> DirPath.repr (dirpath_of_string (ModPath.to_string mp))
+  in
   make_qualid ?loc
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
 let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
-      let (mp,dir,id) = Constant.repr3 cst in
-      encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id)
+      let (mp,id) = Constant.repr2 cst in
+      encode_path ?loc "CST" (Some mp) [] (Label.to_id id)
   | IndRef (kn,i) ->
-      let (mp,dir,id) = MutInd.repr3 kn in
-      encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id]
+      let (mp,id) = MutInd.repr2 kn in
+      encode_path ?loc "IND" (Some mp) [Label.to_id id]
 	(Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
-      let (mp,dir,id) = MutInd.repr3 kn in
-      encode_path ?loc "CSTR" (Some (mp,dir))
+      let (mp,id) = MutInd.repr2 kn in
+      encode_path ?loc "CSTR" (Some mp)
 	[Label.to_id id;Id.of_string ("_"^string_of_int i)]
 	(Id.of_string ("_"^string_of_int j))
   | VarRef id ->
@@ -576,14 +575,14 @@ let raw_string_of_ref ?loc _ = function
 
 let short_string_of_ref ?loc _ = function
   | VarRef id -> qualid_of_ident ?loc id
-  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst)))
-  | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn)))
+  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (Constant.label cst))
+  | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (MutInd.label kn))
   | IndRef (kn,i) ->
-      encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
+      encode_path ?loc "IND" None [Label.to_id (MutInd.label kn)]
         (Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
       encode_path ?loc "CSTR" None
-        [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)]
+        [Label.to_id (MutInd.label kn);Id.of_string ("_"^string_of_int i)]
         (Id.of_string ("_"^string_of_int j))
 
 (* Anticipate that printers can be used from ocamldebug and that