diff options
| -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}\\ \\ |