Strict focusing using Default Goal Selector.

We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.

Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.

Closes #6689.

2 files changed, 20 insertions, 7 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 009758319..7ab11889f 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 7a45272f2..a3d06ae04 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: