diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d806adea5..9ed2e650c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3680,13 +3680,14 @@ adding transparency hints that make the network more constrained (c.f. \ref{HintTransparency}). \begin{Variants} -\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:} +\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$ This is used to declare a hint database that must not be exported to the other modules that require and import the current module. Inside a section, the option {\tt Local} is useless since hints do not survive anyway to the closure of sections. + \end{Variants} The general |