2 files changed, 26 insertions, 8 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 009758319b..7ab11889f5 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 7a45272f25..6c1b1c08c1 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:
 
@@ -627,7 +634,12 @@ puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or
 ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the
 new subgoal is :g:`U`.
 
-If the goal is neither a product nor starting with a let definition,
+If the goal is an existential variable, ``intro`` forces the resolution of the
+existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts
+:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to
+depend on :g:`x`.
+
+If the goal is neither a product, nor starting with a let definition, nor an existential variable,
 the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can
 be applied or the goal is not head-reducible.