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

1 files changed, 2 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.