From f6d4484dfcf538e92241ef27ecc76de8b8ee30ff Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 8 Jan 2020 16:27:54 +0100
Subject: Add note about default goal selector next to bullet docs

Close #11036
---
 doc/sphinx/proof-engine/proof-handling.rst | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc/sphinx/proof-engine')

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" }
-- 
cgit v1.2.3