diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 21 |
3 files changed, 24 insertions, 9 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 1a7628d893..a93e9b156d 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -874,7 +874,7 @@ In the syntax of module application, the ! prefix indicates that any Starts an interactive module satisfying each `module_type`. - .. cmdv:: Module @ident {* @module_binding} <: {+<; @module_type }. + .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. Starts an interactive functor with parameters given by the list of `module_binding`. The output module type is verified against each `module_type`. @@ -1436,7 +1436,9 @@ For instance, the first argument of in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A` will always be inferable from the type :g:`list A` of the third argument of -:g:`cons`. On the contrary, the second argument of a term of type +:g:`cons`. Also, the first argument of :g:`cons` is strict with respect to the second one, +since the first argument is exactly the type of the second argument. +On the contrary, the second argument of a term of type :: forall P:nat->Prop, forall n:nat, P n -> ex nat P diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 009758319b..7ab11889f5 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 7a45272f25..a3d06ae046 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: |