diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 28cb402f35..3e3d422638 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -1427,7 +1427,7 @@ generally any mutually recursive definitions. \begin{Variants} \item {\tt Fixpoint {\ident$_1$} {\params$_1$} :{\type$_1$} := {\term$_1$}\\ with {\ldots} \\ - with {\ident$_m$} {\params$_m$} :{\type$_m$} := {\type$_m$}}\\ + with {\ident$_m$} {\params$_m$} :{\type$_m$} := {\term$_m$}}\\ Allows to define simultaneously {\ident$_1$}, {\ldots}, {\ident$_m$}. \end{Variants} |