14 files changed, 139 insertions, 39 deletions
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 b8bea755e0..c3d895784e 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -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 7870cbb51d..7853866f62 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -175,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 511eaaba9c..50d4d21637 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -252,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/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/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 9d592ee879..f30b4107b6 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,32 @@
 ## Changes between Coq 8.9 and Coq 8.10
 
+### ML API
+
+General deprecation
+
+- 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
 
 ### ML API
@@ -157,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
 
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/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