diff options
| author | letouzey | 2012-08-03 14:35:10 +0000 |
|---|---|---|
| committer | letouzey | 2012-08-03 14:35:10 +0000 |
| commit | 637641a4638c1a5713e036f645cc5ddbbb9eefa5 (patch) | |
| tree | 53b139965724285719bfd1a170399c64253a304e /doc | |
| parent | ddbfd845eadd8ec52eca621b6c4f9848bfe16967 (diff) | |
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
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 10 |
1 files changed, 10 insertions, 0 deletions
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 |