[ssr] better structure the ipats doc

2 files changed, 43 insertions, 21 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 57a0381250..b2f9f7926d 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -163,14 +163,16 @@ SSReflect
   - replace hypothesis: => {}H
   See the reference manual for the actual documentation.
 
-- Clear discipline made consistent: when a clear switch {x..} comes
-  immediately before an existing identifier (used as a view, as a rewrite rule
-  or as name for a new context entry) then such identifier is cleared too.
-  Eg. The following sentences are elaborated as follows:
-  - "=> {x..} H" -> "=> H {x..H}" if H can be cleared
-  - "=> {x..} /v" -> "=> /v {x..v}" if v can be cleared
-  - "rewrite {x..} E" -> "rewrite E {x..E}" if E can be cleared
-
+- Clear discipline made consistent across the entire proof language language.
+  Whenever a clear switch {x..} comes immediately before an existing proof
+  context entry (used as a view, as a rewrite rule or as name for a new
+  context entry) then such entry is cleared too.
+
+  Eg. The following sentences are elaborated as follows (when H is an existing
+  proof context entry):
+  - "=> {x..} H"       ->  "=> {x..H} H"
+  - "=> {x..} /H"      ->  "=> /v {x..H}"
+  - "rewrite {x..} H"  ->  "rewrite E {x..H}"
 
 Changes from 8.8.2 to 8.9+beta1
 ===============================
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index c058279207..d40474188f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1559,7 +1559,7 @@ whose general syntax is
    i_view ::= {? %{%} } /@term %| /ltac:( @tactic )
 
 .. prodn::
-   i_pattern ::= {? %{%} } @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ]
+   i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ]
 
 .. prodn::
    i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ]
@@ -1572,6 +1572,9 @@ The :token:`i_pattern`\s can be seen as a variant of *intro patterns*
 (see :tacn:`intros`:) each performs an introduction operation, i.e., pops some
 variables or assumptions from the goal.
 
+Simplification items
+`````````````````````
+
 An :token:`s_item` can simplify the set of subgoals or the subgoals themselves:
 
 + ``//`` removes all the “trivial” subgoals that can be resolved by the
@@ -1583,12 +1586,15 @@ An :token:`s_item` can simplify the set of subgoals or the subgoals themselves:
   ``/= //``, i.e., ``simpl; try done``.
 
 
-When an :token:`s_item` bears a :token:`clear_switch`, then the
+When an :token:`s_item` immediately precedes a :token:`clear_switch`, then the
 :token:`clear_switch` is executed
 *after* the :token:`s_item`, e.g., ``{IHn}//`` will solve some subgoals,
 possibly using the fact ``IHn``, and will erase ``IHn`` from the context
 of the remaining subgoals.
 
+Views
+`````
+
 The first entry in the :token:`i_view` grammar rule, :n:`/@term`,
 represents a view (see section :ref:`views_and_reflection_ssr`).
 It interprets the top of the stack with the view :token:`term`.
@@ -1612,6 +1618,9 @@ Notations can be used to name tactics,  for example::
 lets one write just ``/myop`` in the intro pattern. Note the scope
 annotation: views are interpreted opening the ``ssripat`` scope.
 
+Intro patterns
+``````````````
+
 |SSR| supports the following :token:`i_pattern`\s:
 
 :token:`ident`
@@ -1621,9 +1630,8 @@ annotation: views are interpreted opening the ``ssripat`` scope.
   required to expose the top variable or assumption.
   A :token:`clear_switch` (even an empty one) immediately preceding a
   :token:`ident` is extended with that :token:`ident` if the identifier
-  points to an existing context entry.
-  In other words by prefixing the :token:`ident` with ``{}`` one can
-  *replace* the context entry.
+  points to an existing context entry. 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.
   Type class instances are popped even if they don't occur
@@ -1717,6 +1725,9 @@ annotation: views are interpreted opening the ``ssripat`` scope.
 Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for
 destructing intro-patterns.
 
+Clear switch
+````````````
+
 Clears are deferred until the end of the intro pattern.
 
 .. example::
@@ -1739,6 +1750,9 @@ is performed behind the scenes.
 Facts mentioned in a clear switch must be valid names in the proof
 context (excluding the section context).
 
+Branching and destructuring
+```````````````````````````
+
 The rules for interpreting branching and destructing :token:`i_pattern` are
 motivated by the fact that it would be pointless to have a branching
 pattern if tactic is a ``move``, and in most of the remaining cases
@@ -1763,6 +1777,9 @@ interpretation, e.g.:
 
 are all equivalent.
 
+Block introduction
+``````````````````
+
 |SSR| supports the following :token:`i_block`\s:
 
 :n:`[^ @ident ]`
@@ -3039,13 +3056,20 @@ operation should be performed:
   pattern. In its simplest form, it is a regular term. If no explicit
   redex switch is present the rewrite pattern to be matched is inferred
   from the :token:`r_item`.
-+ This optional term, or the :token:`r_item`, may be preceded by an occurrence
-  switch (see section :ref:`selectors_ssr`) or a clear item
-  (see section :ref:`discharge_ssr`),
-  these two possibilities being exclusive. An occurrence switch selects
++ This optional term, or the :token:`r_item`, may be preceded by an
+  :token:`occ_switch` (see section :ref:`selectors_ssr`) or a
+  :token:`clear_switch` (see section :ref:`discharge_ssr`),
+  these two possibilities being exclusive.
+
+  An occurrence switch selects
   the occurrences of the rewrite pattern which should be affected by the
   rewrite operation.
 
+  A clear switch, even an empty one, is 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
+  write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately
+  afterwards.
 
 An :token:`r_item` can be:
 
@@ -3300,10 +3324,6 @@ the rewrite tactic. The effect of the tactic on the initial goal is to
 rewrite this lemma at the second occurrence of the first matching
 ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``.
 
-An empty occurrence switch ``{}`` is not interpreted as a valid occurrence
-switch. It has the effect of clearing the :token:`r_item` (when it is the name
-of a context entry).
-
 Occurrence selection and repetition
 ```````````````````````````````````