diff options
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 502b42b837..8b404f4efa 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -24,7 +24,7 @@ construction allows to define ``signatures''. && ~~~~\zeroone{\ident} \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\ & & \\ -{\field} & ::= & {\name} : {\type} \\ +{\field} & ::= & {\name} : {\type} [ {\tt where} {\it notation} ] \\ & $|$ & {\name} {\typecstr} := {\term} \end{tabular} \end{centerframe} |