diff options
| author | Théo Zimmermann | 2019-01-23 14:08:02 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-01-23 14:08:02 +0100 |
| commit | 4aa0dddfba559370fefa6fe1a6e7ffa00c2577c3 (patch) | |
| tree | 881f23714e8e1157f3571829a4986dee7a81a673 | |
| parent | 6be3f746d84028297b5d9888684e716b91cd8824 (diff) | |
Fix the information of the level of ; vs ; [ ]
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 4 |
1 files 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` |