diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 21 |
2 files changed, 20 insertions, 7 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 009758319..7ab11889f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -272,6 +272,12 @@ focused goals with: In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. + .. tacv:: !: @expr + + In this variant, if exactly one goal is focused :n:`expr` is + applied to it. Otherwise the tactical fails. ``!:`` can only be + used at the toplevel of a tactic expression. + .. tacv:: par: @expr In this variant, :n:`@expr` is applied to all focused goals in parallel. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7a45272f2..a3d06ae04 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -53,13 +53,20 @@ specified, the default selector is used. .. opt:: Default Goal Selector @toplevel_selector - This option controls the default selector – used when no selector is - specified when applying a tactic – is set to the chosen value. The initial - value is 1, hence the tactics are, by default, applied to the first goal. - Using value ``all`` will make is so that tactics are, by default, applied to - every goal simultaneously. Then, to apply a tactic tac to the first goal - only, you can write ``1:tac``. Although more selectors are available, only - ``all`` or a single natural number are valid default goal selectors. + This option controls the default selector, used when no selector is + specified when applying a tactic. The initial value is 1, hence the + tactics are, by default, applied to the first goal. + + Using value ``all`` will make it so that tactics are, by default, + applied to every goal simultaneously. Then, to apply a tactic tac + to the first goal only, you can write ``1:tac``. + + Using value ``!`` enforces that all tactics are used either on a + single focused goal or with a local selector (’’strict focusing + mode’’). + + Although more selectors are available, only ``all``, ``!`` or a + single natural number are valid default goal selectors. .. _bindingslist: |