diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 2 |
2 files changed, 8 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 6884b6e998..0527e26353 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -490,6 +490,13 @@ The following example script illustrates all these features: You just finished a goal focused by ``{``, you must unfocus it with ``}``. +Mandatory Bullets +````````````````` + +Using :opt:`Default Goal Selector` with the ``!`` selector forces +tactic scripts to keep focus to exactly one goal (e.g. using bullets) +or use explicit goal selectors. + Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 89b24ea8a3..a38c26c2b3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1200,7 +1200,7 @@ Controlling the locality of commands + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them.For these commands, the Local modifier + when no section contains them. For these commands, the Local modifier limits the effect to the current section or module while the Global modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this |