Add note about default goal selector next to bullet docs

Close #11036

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" }