Document the command Add/Remove Search Blacklist

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

2 files changed, 12 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 78d4c47291..99c349188b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -163,7 +163,7 @@ Tactics
 - New proof engine.
 - Scripts can now be structured thanks to bullets - * + and to subgoal
   delimitation via { }. Note: for use with ProofGeneral, a cvs version of
-  Proof General no older than mid-July 2011 is currently required (DOC TODO).
+  Proof General no older than mid-July 2011 is currently required.
 - Support for tactical "info" is suspended.
 - Support for command "Show Script" is suspended.
 - New tactics constr_eq, is_evar and has_evar for use in Ltac (DOC TODO).
@@ -217,8 +217,7 @@ Vernacular commands
 - New command "Add/Remove Search Blacklist <substring> ..." :
   a Search or SearchAbout or similar query will never mention lemmas
   whose qualified names contain any of the declared substrings.
-  The default blacklisted substrings are "_admitted" "_subproof" "Private_"
-  (DOC TODO).
+  The default blacklisted substrings are "_admitted" "_subproof" "Private_".
 - When the output file of "Print Universes" ends in ".dot" or ".gv",
   the universe graph is printed in the DOT language, and can be
   processed by Graphviz tools.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 4208787fcc..491e61c844 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -336,6 +336,16 @@ This restricts the search to constructions not defined in modules
 
 \end{Variants}
 
+\subsubsection{Nota Bene:}
+For the {\tt Search}, {\tt SearchAbout}, {\tt SearchPattern} and
+{\tt SearchRewrite} queries, it is possible to globally filter
+the search results via the command
+{\tt Add Search Blacklist "substring1"}.
+A lemma whose fully-qualified name contains any of the declared substrings
+will be removed from the search results.
+The default blacklisted substrings are {\tt "\_admitted"
+  "\_subproof" "Private\_"}. The command {\tt Remove Search Blacklist
+  ...} allows to expunge this blacklist.
 
 % \begin{tabbing}
 % \ \ \ \ \=11.\ \=\kill