clarify when an ident is added to the clear switch

1 files changed, 13 insertions, 5 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ae721c2430..d7aa0e1b07 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1601,10 +1601,14 @@ It interprets the top of the stack with the view :token:`term`.
 It is equivalent to :n:`move/@term`.
 
 A :token:`clear_switch` that immediately precedes an :token:`i_view`
-that happen to be a :token:`ident` is extended with that
-:token:`ident` and the :token:`clear_switch` is executed after the view.
+is complemented with the name of the view whenever the :token:`i_view`
+is a simple proof context entry [#10]_.
 E.g. ``{}/v`` is equivalent to ``/v{v}``.
 
+A :token:`clear_switch` that immediately precedes an :token:`i_view`
+is executed after the view application.
+
+
 If the next :token:`i_item` is a view, then the view is
 applied to the assumption in top position once all the
 previous :token:`i_item` have been performed.
@@ -1629,8 +1633,9 @@ Intro patterns
   Note that defined constants cannot be introduced when δ-expansion is
   required to expose the top variable or assumption.
   A :token:`clear_switch` (even an empty one) immediately preceding an
-  :token:`ident` is extended with that :token:`ident` if the identifier
-  points to an existing context entry. As a consequence  by prefixing the
+  :token:`ident` is complemented with that :token:`ident` if the identifier
+  is a simple proof context entry [#10]_.
+  As a consequence  by prefixing the
   :token:`ident` with ``{}`` one can *replace* a context entry.
 ``>``
   pops every variable occurring in the rest of the stack.
@@ -3067,7 +3072,8 @@ operation should be performed:
 
   A clear switch, even an empty one, is performed *after* the
   :token:`r_item` is actually processed and is complemented with the name of
-  the rewrite rule when it is a simple context entry. As a consequence one can
+  the rewrite rule when it is a simple proof context entry [#10]_.
+  As a consequence one can
   write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately
   afterwards.
 
@@ -5549,3 +5555,5 @@ Settings
   in the metatheory
 .. [#9] The current state of the proof shall be displayed by the Show
   Proof command of |Coq| proof mode.
+.. [#10] A simple proof context entry is a naked identifier (i.e. not between
+  parentheses) designating a context entry that is not a section variable.