12 files changed, 37 insertions, 21 deletions
diff --git a/doc/changelog/03-notations/13519-primitiveArrayNotations.rst b/doc/changelog/03-notations/13519-primitiveArrayNotations.rst
new file mode 100644
index 0000000000..fb2545652c
--- /dev/null
+++ b/doc/changelog/03-notations/13519-primitiveArrayNotations.rst
@@ -0,0 +1,8 @@
+- **Added:**
+  :cmd:`Number Notation` and :cmd:`String Notation` now support
+  parsing and printing of primitive floats, primitive arrays
+  and type constants of primitive types.
+  (`#13519 <https://github.com/coq/coq/pull/13519>`_,
+  fixes `#13484 <https://github.com/coq/coq/issues/13484>`_
+  and `#13517 <https://github.com/coq/coq/issues/13517>`_,
+  by Fabian Kunze, with help of Jason Gross)
diff --git a/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst b/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst
new file mode 100644
index 0000000000..06c1e280c3
--- /dev/null
+++ b/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst
@@ -0,0 +1,6 @@
+- **Removed:**
+  Deprecated flag ``Bracketing Last Introduction Pattern`` affecting the
+  behavior of trailing disjunctive introduction patterns is
+  definitively removed
+  (`#13509 <https://github.com/coq/coq/pull/13509>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/07-commands-and-options/00000-title.rst b/doc/changelog/07-vernac-commands-and-options/00000-title.rst
index fe50ae0e16..fe50ae0e16 100644
--- a/doc/changelog/07-commands-and-options/00000-title.rst
+++ b/doc/changelog/07-vernac-commands-and-options/00000-title.rst
diff --git a/doc/changelog/07-commands-and-options/13556-master.rst b/doc/changelog/07-vernac-commands-and-options/13556-master.rst
index 05a60026a3..05a60026a3 100644
--- a/doc/changelog/07-commands-and-options/13556-master.rst
+++ b/doc/changelog/07-vernac-commands-and-options/13556-master.rst
diff --git a/doc/changelog/08-cli-tools/00000-title.rst b/doc/changelog/08-cli-tools/00000-title.rst
new file mode 100644
index 0000000000..4c0de43f66
--- /dev/null
+++ b/doc/changelog/08-cli-tools/00000-title.rst
@@ -0,0 +1,4 @@
+
+Command-line tools
+^^^^^^^^^^^^^^^^^^
+
diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst
deleted file mode 100644
index 581585a8a7..0000000000
--- a/doc/changelog/08-tools/00000-title.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-
-Tools
-^^^^^
-
diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst
new file mode 100644
index 0000000000..27d89b2f8b
--- /dev/null
+++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+  Minor Changes to Rpower:
+  Generalizes exp_ineq1 to hold for all non-zero numbers.
+  Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <).
+
+  (`#13582 <https://github.com/coq/coq/pull/13582>`_,
+  by Avi Shinnar and Barry Trager, with help from Laurent Théry
+
+).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 726a6309d4..fcb150e3da 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -370,7 +370,8 @@ Notations
   by Pierre Roux, review by Jason Gross and Jim Fehrle for the
   reference manual).
 - **Added:**
-  Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t`
+  Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t`.
+  This feature is considered experimental.
   (`#12765 <https://github.com/coq/coq/pull/12765>`_,
   by Hugo Herbelin).
 - **Added:**
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 246568d3c1..bce88cebde 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -220,7 +220,7 @@ html_context = {
         ("dev", "https://coq.github.io/doc/master/refman/"),
         ("stable", "https://coq.inria.fr/distrib/current/refman/"),
         ("v8.13", "https://coq.github.io/doc/v8.13/refman/"),
-        ("8.12", "https://coq.inria.fr/distrib/V8.12.1/refman/"),
+        ("8.12", "https://coq.inria.fr/distrib/V8.12.2/refman/"),
         ("8.11", "https://coq.inria.fr/distrib/V8.11.2/refman/"),
         ("8.10", "https://coq.inria.fr/distrib/V8.10.2/refman/"),
         ("8.9", "https://coq.inria.fr/distrib/V8.9.1/refman/"),
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 8f5c045929..d8c4fb61c2 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -264,17 +264,6 @@ These patterns can be used when the hypothesis is an equality:
   :n:`@simple_intropattern_closed`.
   :ref:`Example <intropattern_injection_ex>`
 
-.. flag:: Bracketing Last Introduction Pattern
-
-   For :n:`intros @intropattern_list`, controls how to handle a
-   conjunctive pattern that doesn't give enough simple patterns to match
-   all the arguments in the constructor.  If set (the default), Coq generates
-   additional names to match the number of arguments.
-   Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more
-   similar to |SSR|'s intro patterns.
-
-   .. deprecated:: 8.10
-
 .. _intropattern_cons_note:
 
 .. note::
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index b7f2927000..3649202b45 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -522,7 +522,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
      use the name of the constant the (co)fixpoint comes from instead of
      the (co)fixpoint definition in recursive calls.
 
-   The :tacn:`cbn` tactic is claimed to be a more principled, faster and more
+   The :tacn:`cbn` tactic was intended to be a more principled, faster and more
    predictable replacement for :tacn:`simpl`.
 
    The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 73f90b0056..f454f4313d 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -857,7 +857,8 @@ example showing a notation for a chain of equalities. It relies on an
 artificial expansion of the intended denotation so as to expose a
 ``φ(x, .. φ(y,t) ..)`` structure, with the drawback that if ever the
 beta-redexes are contracted, the notations stops to be used for
-printing.
+printing. Support for notations defined in this way should be considered
+experimental.
 
 .. coqtop:: in
 
@@ -1740,7 +1741,8 @@ Number notations
 
          Note that only fully-reduced ground terms (terms containing only
          function application, constructors, inductive type families,
-         sorts, and primitive integers) will be considered for printing.
+         sorts, primitive integers, primitive floats, primitive arrays and type
+         constants for primitive types) will be considered for printing.
 
       .. _number-string-via:
 
@@ -1904,7 +1906,8 @@ String notations
 
          Note that only fully-reduced ground terms (terms containing only
          function application, constructors, inductive type families,
-         sorts, and primitive integers) will be considered for printing.
+         sorts, primitive integers, primitive floats, primitive arrays and type
+         constants for primitive types) will be considered for printing.
 
       :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
          works as for :ref:`number notations above <number-string-via>`.