diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-26 13:15:55 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-05 11:54:06 +0200 |
| commit | 482594f4b2c8360a75acf59d756601e3ac4a0046 (patch) | |
| tree | 9023cc90625e312cd319860bb351fa5f33a4e0fb /doc/sphinx/proof-engine/ltac.rst | |
| parent | 830a2e508ca951757dbe7923407f5d02442a4920 (diff) | |
[sphinx] Add indices for only, all and par.
Diffstat (limited to 'doc/sphinx/proof-engine/ltac.rst')
| -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 |