Merge PR #12927: Explain that tactics applied to multiple goals don't preserve the order

Reviewed-by: Zimmi48
Ack-by: chdoc
Ack-by: jfehrle

2 files changed, 37 insertions, 10 deletions

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/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index f3dc9a6cb1..72c6ec4ac5 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:
@@ -4751,9 +4751,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 +4775,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 +4794,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::