diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 7 |
1 files changed, 7 insertions, 0 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" } |