9 files changed, 49 insertions, 27 deletions
diff --git a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst
new file mode 100644
index 0000000000..b719c5618e
--- /dev/null
+++ b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  Deprecated ``cutrewrite`` tactic. Use :tacn:`replace` instead
+  (`#12993 <https://github.com/coq/coq/pull/12993>`_,
+  by Théo Zimmermann).
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 34752a4c4d..182f599a29 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -880,10 +880,10 @@ Here is a summary of the error messages corresponding to each
 situation:
 
 .. exn:: The constructor @ident expects @num arguments.
+         The variable ident is bound several times in pattern term
+         Found a constructor of inductive type term while a constructor of term is expected
 
-   The variable ident is bound several times in pattern termFound a constructor
-   of inductive type term while a constructor of term is expectedPatterns are
-   incorrect (because constructors are not applied to the correct number of the
+   Patterns are incorrect (because constructors are not applied to the correct number of
    arguments, because they are not linear or they are wrongly typed).
 
 .. exn:: Non exhaustive pattern matching.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index e7ba82fb31..d8b2af092f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -375,8 +375,14 @@ behavior.)
       | !
       | par
 
-   Applies :token:`ltac_expr` to the selected goals.  It can only be used at the top
-   level of a tactic expression; it cannot be used within a tactic expression.
+   Reorders the goals and applies :token:`ltac_expr` to the selected goals.  It can
+   only be used at the top level of a tactic expression; it cannot be used within a
+   tactic expression.  The selected goals are reordered so they appear after the
+   lowest-numbered selected goal, ordered by goal number.  :ref:`Example
+   <reordering_goals_ex>`.  If the selector applies
+   to a single goal or to all goals, the reordering will not be apparent.  The order of
+   the goals in the :token:`selector` is irrelevant.  (This may not be what you expect;
+   see `#8481 <https://github.com/coq/coq/issues/8481>`_.)
 
    .. todo why shouldn't "all" and "!" be accepted anywhere a @selector is accepted?
       It would be simpler to explain.
@@ -430,6 +436,19 @@ Selectors can also be used nested within a tactic expression with the
    :name: No such goal. (Goal selector)
    :undocumented:
 
+.. _reordering_goals_ex:
+
+.. example:: Selector reordering goals
+
+   .. coqtop:: reset in
+
+      Goal 1=0 /\ 2=0 /\ 3=0.
+
+   .. coqtop:: all
+
+      repeat split.
+      1,3: idtac.
+
 .. TODO change error message index entry
 
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 4480b10319..55e4f26fe8 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -156,6 +156,10 @@ list of assertion commands is given in :ref:`Assertions`. The command
    ``T``, then the commands ``Proof using a`` and ``Proof using T a``
    are equivalent.
 
+   The set of declared variables always includes the variables used by
+   the statement. In other words ``Proof using e`` is equivalent to
+   ``Proof using Type + e`` for any declaration expression ``e``.
+
    .. cmdv:: Proof using {+ @ident } with @tactic
 
       Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7f270e8076..5a11b4f474 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3110,7 +3110,7 @@ An :token:`r_item` can be:
     + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above.
       The tactic: ``rewrite r_prefix (t1 ,…,tn ).``
       is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].``
-    + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above.  tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``.
+    + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above.
 
   .. example::
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index f3dc9a6cb1..2211a58e6e 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -54,7 +54,7 @@ Invocation of tactics
 ~~~~~~~~~~~~~~~~~~~~~
 
 A tactic is applied as an ordinary command. It may be preceded by a
-goal selector (see Section :ref:`ltac-semantics`). If no selector is
+goal selector (see Section :ref:`goal-selectors`). If no selector is
 specified, the default selector is used.
 
 .. _tactic_invocation_grammar:
@@ -2819,13 +2819,6 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       only in the conclusion of the goal. The clause argument must not contain
       any ``type of`` nor ``value of``.
 
-   .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident }
-      :name: cutrewrite
-
-      .. deprecated:: 8.5
-
-         Use :tacn:`replace` instead.
-
 .. tacn:: subst @ident
    :name: subst
 
@@ -4751,9 +4744,13 @@ Non-logical tactics
 .. tacn:: cycle @num
    :name: cycle
 
-   This tactic puts the :n:`@num` first goals at the end of the list of goals.
-   If :n:`@num` is negative, it will put the last :math:`|num|` goals at the
+   Reorders the selected goals so that the first :n:`@num` goals appear after the
+   other selected goals.
+   If :n:`@num` is negative, it puts the last :n:`@num` goals at the
    beginning of the list.
+   The tactic is only useful with a goal selector, most commonly `all:`.
+   Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent
+   to `all: cycle 1`.  See :tacn:`… : … (goal selector)`.
 
 .. example::
 
@@ -4771,10 +4768,12 @@ Non-logical tactics
 .. tacn:: swap @num @num
    :name: swap
 
-   This tactic switches the position of the goals of indices :n:`@num` and
-   :n:`@num`.  Negative values for:n:`@num` indicate counting goals
-   backward from the end of the focused goal list. Goals are indexed from 1,
-   there is no goal with position 0.
+   Exchanges the position of the specified goals.
+   Negative values for :n:`@num` indicate counting goals
+   backward from the end of the list of selected goals. Goals are indexed from 1.
+   The tactic is only useful with a goal selector, most commonly `all:`.
+   Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent
+   to `all: swap 1 3`.  See :tacn:`… : … (goal selector)`.
 
 .. example::
 
@@ -4788,7 +4787,9 @@ Non-logical tactics
 .. tacn:: revgoals
    :name: revgoals
 
-   This tactics reverses the list of the focused goals.
+   Reverses the order of the selected goals.  The tactic is only useful with a goal
+   selector, most commonly `all :`.   Note that other selectors reorder goals;
+   `1,3: revgoals` is not equivalent to `all: revgoals`.  See :tacn:`… : … (goal selector)`.
 
    .. example::
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 6625e07d05..9971a03894 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1033,9 +1033,6 @@ simple_tactic: [
 | DELETE "unify" constr constr
 | REPLACE "unify" constr constr "with" preident
 | WITH "unify" constr constr OPT ( "with" preident )
-| DELETE "cutrewrite" orient constr
-| REPLACE "cutrewrite" orient constr "in" hyp
-| WITH "cutrewrite" orient constr OPT ( "in" hyp )
 | DELETE "destauto"
 | REPLACE "destauto" "in" hyp
 | WITH "destauto" OPT ( "in" hyp )
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 7f4e92fc37..f628c86cf1 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1535,8 +1535,6 @@ simple_tactic: [
 | "simple" "injection" destruction_arg
 | "dependent" "rewrite" orient constr
 | "dependent" "rewrite" orient constr "in" hyp
-| "cutrewrite" orient constr
-| "cutrewrite" orient constr "in" hyp
 | "decompose" "sum" constr
 | "decompose" "record" constr
 | "absurd" constr
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 84efc1e36c..3cd5a85654 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1445,7 +1445,6 @@ simple_tactic: [
 | "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
 | "simple" "injection" OPT destruction_arg
 | "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
-| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
 | "decompose" "sum" one_term
 | "decompose" "record" one_term
 | "absurd" one_term