aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman')
-rw-r--r--doc/refman/RefMan-tac.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4b06520314..3f12411863 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -114,7 +114,7 @@ following syntax:
\begin{tabular}{lcl}
{\occclause} & ::= & {\tt in} {\occgoalset} \\
{\occgoalset} & ::= &
- \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
+ \zeroonelax{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
& & {\dots} {\tt ,}\\
& & {\ident$_m$} \zeroone{\atoccurrences}}\\
& & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\