From 6be3f746d84028297b5d9888684e716b91cd8824 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 23 Jan 2019 13:03:10 +0100
Subject: Improve the note in the beginning of the Ltac chapter.

In particular, add an example to illustrate the associativity of ;
---
 doc/sphinx/proof-engine/ltac.rst | 40 ++++++++++++++++++++++------------------
 1 file changed, 22 insertions(+), 18 deletions(-)

(limited to 'doc')

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`
-- 
cgit v1.2.3


From 4aa0dddfba559370fefa6fe1a6e7ffa00c2577c3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 23 Jan 2019 14:08:02 +0100
Subject: Fix the information of the level of ; vs ; [ ]

---
 doc/sphinx/proof-engine/ltac.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 91edf271f3..127f89f202 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -62,7 +62,7 @@ mode but it can also be used in toplevel definitions as shown below.
    - 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  ``… ; …`` .
+     which binds at the same level as  ``… ; …`` .
 
      .. example::
 
@@ -70,7 +70,7 @@ mode but it can also be used in toplevel definitions as shown below.
 
         is understood as:
 
-        :n:`try (repeat (@tactic__1 || @tactic__2)); ((@tactic__3; [ {+| @tactic }]); @tactic__4)`
+        :n:`((try (repeat (@tactic__1 || @tactic__2)); @tactic__3); [ {+| @tactic } ]); @tactic__4`
 
 .. productionlist::  coq
    expr              : `expr` ; `expr`
-- 
cgit v1.2.3