aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-syn.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index ed54ecb670..548c259856 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -463,7 +463,7 @@ Locate "'exists' _ , _".
\nelist{{\cofixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\
\\
{\declnotation} & ::= &
- \zeroone{{\tt where} {\str} {\tt :=} {\term} \zeroone{:{\scope}}} .
+ \zeroone{{\tt where} \nelist{{\str} {\tt :=} {\term} \zeroone{:{\scope}}}{\tt and}}.
\\
\\
{\modifiers}