10 files changed, 80 insertions, 30 deletions
diff --git a/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst
new file mode 100644
index 0000000000..aaacb2aadf
--- /dev/null
+++ b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Possible collision between a user-level name and an internal name when
+  using the :n:`%` introduction pattern
+  (`#13512 <https://github.com/coq/coq/pull/13512>`_,
+  fixes `#13413 <https://github.com/coq/coq/issues/13413>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/13699-fix13579.rst b/doc/changelog/04-tactics/13699-fix13579.rst
new file mode 100644
index 0000000000..9cf62fb595
--- /dev/null
+++ b/doc/changelog/04-tactics/13699-fix13579.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  :tacn:`simpl` and :tacn:`hnf` now reduce primitive functions
+  on primitive integers, floats and arrays
+  (`#13699 <https://github.com/coq/coq/pull/13699>`_,
+  fixes `#13579 <https://github.com/coq/coq/issues/13579>`_,
+  by Pierre Roux).
diff --git a/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst
new file mode 100644
index 0000000000..653e9cd0cd
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  :cmd:`Hint Rewrite` now supports locality attributes (including :attr:`export`) like other :ref:`Hint <creating_hints>` commands
+  (`#13725 <https://github.com/coq/coq/pull/13725>`_,
+  fixes `#13724 <https://github.com/coq/coq/issues/13724>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index c54db36691..9ac05fab2e 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -726,6 +726,30 @@ declare your constant as rigid for proof search using the command
 Strategies for rewriting
 ------------------------
 
+Usage
+~~~~~
+
+.. tacn:: rewrite_strat @rewstrategy {? in @ident }
+   :name: rewrite_strat
+
+   Rewrite using :n:`@rewstrategy` in the conclusion or in the hypothesis :n:`@ident`.
+
+   .. exn:: Nothing to rewrite.
+
+      The strategy didn't find any matches.
+
+   .. exn:: No progress made.
+
+      If the strategy succeeded but made no progress.
+
+   .. exn:: Unable to satisfy the rewriting constraints.
+
+      If the strategy succeeded and made progress but the
+      corresponding rewriting constraints are not satisfied.
+
+   :tacn:`setoid_rewrite` :n:`@one_term` is basically equivalent to
+   :n:`rewrite_strat outermost @one_term`.
+
 Definitions
 ~~~~~~~~~~~
 
@@ -773,7 +797,7 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`.
    failure
 
 :n:`id`
-  identity
+   identity
 
 :n:`refl`
    reflexivity
@@ -803,10 +827,16 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`.
    all subterms
 
 :n:`innermost @rewstrategy`
-   innermost first
+   Innermost first.
+   When there are multiple nested matches in a subterm, the innermost subterm
+   is rewritten.  For :ref:`example <rewrite_strat_innermost_outermost>`,
+   rewriting :n:`(a + b) + c` with Nat.add_comm gives :n:`(b + a) + c`.
 
 :n:`outermost @rewstrategy`
-   outermost first
+   Outermost first.
+   When there are multiple nested matches in a subterm, the outermost subterm
+   is rewritten.  For :ref:`example <rewrite_strat_innermost_outermost>`,
+   rewriting :n:`(a + b) + c` with Nat.add_comm gives :n:`c + (a + b)`.
 
 :n:`bottomup @rewstrategy`
    bottom-up
@@ -833,8 +863,8 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`.
    to be documented
 
 
-A few of these are defined in terms of the others using a
-primitive fixpoint operator:
+Conceptually, a few of these are defined in terms of the others using a
+primitive fixpoint operator `fix`, which the tactic doesn't currently support:
 
 - :n:`try @rewstrategy := choice @rewstrategy id`
 - :n:`any @rewstrategy := fix @ident. try (@rewstrategy ; @ident)`
@@ -876,30 +906,30 @@ if it reduces the subterm under consideration. The ``fold`` strategy takes
 a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term`
 on success. It is stronger than the tactic ``fold``.
 
+.. _rewrite_strat_innermost_outermost:
 
-Usage
-~~~~~
-
-
-.. tacn:: rewrite_strat @rewstrategy {? in @ident }
-   :name: rewrite_strat
+.. example:: :n:`innermost` and :n:`outermost`
 
-   Rewrite using the strategy s in hypothesis ident or the conclusion.
+   The type of `Nat.add_comm` is `forall n m : nat, n + m = m + n`.
 
-   .. exn:: Nothing to rewrite.
+   .. coqtop:: all
 
-      If the strategy failed.
+      Require Import Coq.Arith.Arith.
+      Set Printing Parentheses.
+      Goal forall a b c: nat, a + b + c = 0.
+      rewrite_strat innermost Nat.add_comm.
 
-   .. exn:: No progress made.
+   .. coqtop:: none
 
-      If the strategy succeeded but made no progress.
+      Abort.
+      Goal forall a b c: nat, a + b + c = 0.
 
-   .. exn:: Unable to satisfy the rewriting constraints.
+   Using :n:`outermost` instead gives this result:
 
-      If the strategy succeeded and made progress but the
-      corresponding rewriting constraints are not satisfied.
+   .. coqtop:: all
 
+      rewrite_strat outermost Nat.add_comm.
 
-   The ``setoid_rewrite c`` tactic is basically equivalent to
-   ``rewrite_strat (outermost c)``.
+   .. coqtop:: none
 
+      Abort.
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index b63ae32311..2046788ef3 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -339,7 +339,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in
 
-      Hint Rewrite Ack0 Ack1 Ack2 : base0.
+      Global Hint Rewrite Ack0 Ack1 Ack2 : base0.
 
    .. coqtop:: all
 
@@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in
 
-      Hint Rewrite g0 g1 g2 using lia : base1.
+      Global Hint Rewrite g0 g1 g2 using lia : base1.
 
    .. coqtop:: in
 
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 3646a32a79..1bb4216e4f 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -554,7 +554,7 @@ Built-in quotations
    ltac2_quotations ::= ident : ( @lident )
    | constr : ( @term )
    | open_constr : ( @term )
-   | pattern : ( @cpattern )
+   | pat : ( @cpattern )
    | reference : ( {| & @ident | @qualid } )
    | ltac1 : ( @ltac1_expr_in_env )
    | ltac1val : ( @ltac1_expr_in_env )
@@ -568,7 +568,7 @@ The current implementation recognizes the following built-in quotations:
   (type ``Init.constr``).
 - ``open_constr``, which parses Coq terms and produces a term potentially with
   holes at runtime (type ``Init.constr`` as well).
-- ``pattern``, which parses Coq patterns and produces a pattern used for term
+- ``pat``, which parses Coq patterns and produces a pattern used for term
   matching (type ``Init.pattern``).
 - ``reference``  Qualified names
   are globalized at internalization into the corresponding global reference,
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index d7228a3907..d2e88261ae 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -273,12 +273,15 @@ Creating Hints
      :cmd:`Import` or :cmd:`Require` the current module.
 
    + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current
-     module, but not when they only :cmd:`Require` it. This attribute is supported by
-     all `Hint` commands except for :cmd:`Hint Rewrite`.
+     module, but not when they only :cmd:`Require` it.
 
    + :attr:`global` hints are visible from other modules when they :cmd:`Import` or
      :cmd:`Require` the current module.
 
+   .. versionadded:: 8.14
+
+      The :cmd:`Hint Rewrite` now supports locality attributes like other `Hint` commands.
+
    .. deprecated:: 8.13
 
      The default value for hint locality will change in a future
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 44bb767011..8aeb2e564d 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -2066,7 +2066,7 @@ ltac2_tactic_atom: [
 | MOVETO ltac2_quotations "constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "open_constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
-| MOVETO ltac2_quotations "pattern" ":" "(" cpattern ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "pat" ":" "(" cpattern ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 9f2559ffbc..ec23ffe83e 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -3370,7 +3370,7 @@ G_LTAC2_tactic_atom: [
 | "constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
 | "open_constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
 | "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
-| "pattern" ":" "(" Constr.cpattern ")"      (* Ltac2 plugin *)
+| "pat" ":" "(" Constr.cpattern ")"      (* Ltac2 plugin *)
 | "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
 | "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
 | "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index b53af609ec..75b32a5800 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -2378,7 +2378,7 @@ ltac2_quotations: [
 | "ident" ":" "(" lident ")"
 | "constr" ":" "(" term ")"
 | "open_constr" ":" "(" term ")"
-| "pattern" ":" "(" cpattern ")"
+| "pat" ":" "(" cpattern ")"
 | "reference" ":" "(" [ "&" ident | qualid ] ")"
 | "ltac1" ":" "(" ltac1_expr_in_env ")"
 | "ltac1val" ":" "(" ltac1_expr_in_env ")"