9 files changed, 25 insertions, 9 deletions
diff --git a/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst b/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst
new file mode 100644
index 0000000000..7bcbb9a8e3
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst
@@ -0,0 +1,3 @@
+- **Added:** Support for universe bindings and universe contrainsts in
+  :cmd:`Let` definitions (`#11534
+  <https://github.com/coq/coq/pull/11534>`_, by Théo Zimmermann).
diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
new file mode 100644
index 0000000000..affb685fcb
--- /dev/null
+++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  Confusingly-named and deprecated since 8.11 `-require` option.
+  Use the equivalent `-require-import` instead
+  (`#12005 <https://github.com/coq/coq/pull/12005>`_,
+  by Théo Zimmermann).
diff --git a/doc/changelog/08-tools/12006-issue5632.rst b/doc/changelog/08-tools/12006-issue5632.rst
new file mode 100644
index 0000000000..162d56b1b6
--- /dev/null
+++ b/doc/changelog/08-tools/12006-issue5632.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  ``Makefile`` generated by ``coq_makefile`` erases ``.lia.cache`` and ``.nia.cache`` by ``make cleanall``.
+  (`#12006 <https://github.com/coq/coq/pull/12006>`_,
+  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/11909-fix-≡-level.rst b/doc/changelog/10-standard-library/11909-fix-≡-level.rst
new file mode 100644
index 0000000000..96551be537
--- /dev/null
+++ b/doc/changelog/10-standard-library/11909-fix-≡-level.rst
@@ -0,0 +1,7 @@
+- **Changed:**
+  The level of :g:`≡` in ``Coq.Numbers.Cyclic.Int63.Int63`` is now 70,
+  no associativity, in line with :g:`=`.  Note that this is a minor
+  incompatibility with developments that declare their own :g:`≡`
+  notation and import ``Int63`` (fixes `#11905
+  <https://github.com/coq/coq/issues/11905>`_, `#11909
+  <https://github.com/coq/coq/pull/11909>`_, by Jason Gross).
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index 9ad8df2b1b..df50dbafe3 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -72,7 +72,7 @@ Sections create local contexts which can be shared across multiple definitions.
    Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
    appear inside a section are canceled when the section is closed.
 
-.. cmd:: Let @ident @def_body
+.. cmd:: Let @ident_decl @def_body
          Let Fixpoint @fix_definition {* with @fix_definition }
          Let CoFixpoint @cofix_definition {* with @cofix_definition }
    :name: Let; Let Fixpoint; Let CoFixpoint
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index aa4b6edd7d..958d295219 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -164,6 +164,8 @@ and ``coqtop``, unless stated otherwise:
   it is executed.
 :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This
   is equivalent to running :cmd:`Require` :n:`qualid`.
+:-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`.
+  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
 :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
   This is equivalent to running :cmd:`Require Import` :n:`@qualid`.
 :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
@@ -172,7 +174,6 @@ and ``coqtop``, unless stated otherwise:
   This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
 :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
   This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`.
-:-require *qualid*: Deprecated; use ``-ri`` *qualid*.
 :-batch: Exit just after argument parsing. Available for ``coqtop`` only.
 :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option
   implies -batch (exit just after argument parsing). It is available only
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index b22c5286fe..dacfcb3d5f 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -668,9 +668,7 @@ file is a particular case of module called *library file*.
 .. cmd:: Print Libraries
 
    This command displays the list of library files loaded in the
-   current |Coq| session. For each of these libraries, it also tells if it
-   is imported.
-
+   current |Coq| session.
 
 .. cmd:: Declare ML Module {+ @string }
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 272d17bb35..dc7e0fba37 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -773,7 +773,7 @@ gallina: [
 | assumption_token inline assum_list
 | assumptions_token inline assum_list
 | def_token ident_decl def_body
-| "Let" identref def_body
+| "Let" ident_decl def_body
 | finite_token LIST1 inductive_definition SEP "with"
 | "Fixpoint" LIST1 rec_definition SEP "with"
 | "Let" "Fixpoint" LIST1 rec_definition SEP "with"
@@ -1027,7 +1027,6 @@ gallina_ext: [
 | "Module" "Type" identref LIST0 module_binder check_module_types is_module_type
 | "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl
 | "Section" identref
-| "Chapter" identref
 | "End" identref
 | "Collection" identref ":=" section_subset_expr
 | "Require" export_token LIST1 global
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 0c9d7a853b..535976b7d9 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -851,7 +851,7 @@ command: [
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
 | assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
 | [ "Definition" | "Example" ] ident_decl def_body
-| "Let" ident def_body
+| "Let" ident_decl def_body
 | "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 | "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
 | "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
@@ -873,7 +873,6 @@ command: [
 | "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
 | "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
 | "Section" ident
-| "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid