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(-)

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