Documenting the Remove Hints command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16648 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9aa53eb2b..a091da2df 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3677,6 +3677,14 @@ Furthermore, you are advised not to put your own hints in the
 {\tt core} database, but use one or several databases specific to your
 development.
 
+\subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$
+  \mbox{\dots} \ident$_m$}
+\label{PrintHint}
+\comindex{Remove Hints}
+
+This command removes the hints associated to terms \term$_1$ \mbox{\dots}
+\term$_n$ in databases \ident$_1$ \mbox{\dots} \ident$_m$.
+
 \subsection{\tt Print Hint}
 \label{PrintHint}
 \comindex{Print Hint}