Improve the note in the beginning of the Ltac chapter.

In particular, add an example to illustrate the associativity of ;

1 files changed, 22 insertions, 18 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 1071682ead..91edf271f3 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -41,32 +41,36 @@ mode but it can also be used in toplevel definitions as shown below.
 
 .. note::
 
-   - The infix tacticals “… \|\| …”, “… + …”, and “… ; …” are associative.
+   - The infix tacticals  ``… || …`` ,  ``… + …`` , and  ``… ; …``  are associative.
 
-   - In :token:`tacarg`, there is an overlap between qualid as a direct tactic
-     argument and :token:`qualid` as a particular case of term. The resolution is
-     done by first looking for a reference of the tactic language and if
-     it fails, for a reference to a term. To force the resolution as a
-     reference of the tactic language, use the form :g:`ltac:(@qualid)`. To
-     force the resolution as a reference to a term, use the syntax
-     :g:`(@qualid)`.
+     .. example::
 
-   - As shown by the figure, tactical ``\|\|`` binds more than the prefix
-     tacticals try, repeat, do and abstract which themselves bind more
-     than the postfix tactical “… ;[ … ]” which binds more than “… ; …”.
+        If you want that :n:`@tactic__2; @tactic__3` be fully run on the first
+        subgoal generated by :n:`@tactic__1`, before running on the other
+        subgoals, then you should not write
+        :n:`@tactic__1; (@tactic__2; @tactic__3)` but rather
+        :n:`@tactic__1; [> @tactic__2; @tactic__3 .. ]`.
 
-     For instance
+   - In :token:`tacarg`, there is an overlap between :token:`qualid` as a
+     direct tactic argument and :token:`qualid` as a particular case of
+     :token:`term`. The resolution is done by first looking for a reference
+     of the tactic language and if it fails, for a reference to a term.
+     To force the resolution as a reference of the tactic language, use the
+     form :n:`ltac:(@qualid)`. To force the resolution as a reference to a
+     term, use the syntax :n:`(@qualid)`.
 
-     .. coqtop:: in
+   - As shown by the figure, tactical  ``… || …``  binds more than the prefix
+     tacticals :tacn:`try`, :tacn:`repeat`, :tacn:`do` and :tacn:`abstract`
+     which themselves bind more than the postfix tactical  ``… ;[ … ]`` 
+     which binds more than  ``… ; …`` .
 
-        try repeat tac1 || tac2; tac3; [tac31 | ... | tac3n]; tac4.
+     .. example::
 
-     is understood as
+        :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; [ {+| @tactic } ]; @tactic__4`
 
-     .. coqtop:: in
+        is understood as:
 
-        try (repeat (tac1 || tac2));
-          ((tac3; [tac31 | ... | tac3n]); tac4).
+        :n:`try (repeat (@tactic__1 || @tactic__2)); ((@tactic__3; [ {+| @tactic }]); @tactic__4)`
 
 .. productionlist::  coq
    expr              : `expr` ; `expr`