diff options
Diffstat (limited to 'doc/refman/RefMan-mod.tex')
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index eff98d588..68d572265 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -160,9 +160,9 @@ This command is used to start an interactive module type {\ident}. is a shortcut for {\tt Include {\module$_1$}} $\ldots$ {\tt Include {\module$_n$}} -\item {\tt {\declarationkeyword} Inline {\assums} } +\item {\tt {\assumptionkeyword} Inline {\assums} } - This declaration will be automatically unfolded at functor + The instance of this assumption will be automatically expanded at functor application, except when this functor application is prefixed by a $!$ annotation. \end{enumerate} \subsection{\tt End {\ident} |