From 86e8e098e8ea99a0167ba3e672a34d8a4763205b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 1 Aug 2013 15:35:26 +0000
Subject: Documenting the Remove Hints command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16648 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9aa53eb2be..a091da2df7 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}
-- 
cgit v1.2.3