diff options
-rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d81048f07..c5ee724ca 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -245,9 +245,10 @@ focused goals with: :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested - in a tactic expression, by using the keyword ``only``: + in a tactic expression, by using the keyword :tacn:`only`: .. tacv:: only selector : expr + :name: only ... : ... When selecting several goals, the tactic expr is applied globally to all selected goals. @@ -268,6 +269,7 @@ focused goals with: for ``n-n`` when specifying multiple ranges. .. tacv:: all: @expr + :name: all: ... In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. @@ -279,6 +281,7 @@ focused goals with: used at the toplevel of a tactic expression. .. tacv:: par: @expr + :name: par: ... In this variant, :n:`@expr` is applied to all focused goals in parallel. The number of workers can be controlled via the command line option |