diff options
| author | Arnaud Spiwack | 2015-01-14 14:50:31 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-01-14 15:00:03 +0100 |
| commit | cdd37b4a3d29e85c0538833b06ceac2140fa4ecc (patch) | |
| tree | 593ab7dc2e0b0712971698d18cb496dc1450092a | |
| parent | 529fe7397b78fc4670073ed213667bd781aabc17 (diff) | |
Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].
| -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 73bcc85871..b90e682df1 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}\\ \\ |