From 637641a4638c1a5713e036f645cc5ddbbb9eefa5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 3 Aug 2012 14:35:10 +0000
Subject: 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
---
 doc/refman/RefMan-oth.tex | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'doc')

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
-- 
cgit v1.2.3