diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ff85b629b1..465ee925ee 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4091,7 +4091,7 @@ the tactic. No database name is given: the hint is registered in the {\tt core} database. -\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 hints that must not be exported to the other @@ -4099,7 +4099,7 @@ the tactic. section, the option {\tt Local} is useless since hints do not survive anyway to the closure of sections. -\item\texttt{Hint Local} \textsl{hint\_definition} +\item\texttt{Local Hint} \textsl{hint\_definition} Idem for the {\tt core} database. |