diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-01-14 14:50:31 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-01-14 14:50:58 +0100 |
| commit | 3c0e842a133a9da088a9f0fe0fb9b0e699f984ac (patch) | |
| tree | 05238cc1f7d806b066a8821641275263a4d5a894 /doc/refman/RefMan-ltac.tex | |
| parent | 9e809796dda907f39c4792a247d3156433de4fc4 (diff) | |
Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 73bcc8587..b90e682df 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -91,6 +91,7 @@ is understood as \begin{tabular}{lcl} {\tacexpr} & ::= & {\tacexpr} {\tt ;} {\tacexpr}\\ +& | & {\tt [>} \nelist{\tacexpr}{|} {\tt ]}\\ & | & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\ & | & {\tacexprpref}\\ \\ |