SearchAbout and similar: add a customizable blacklist

 Instead of hard-coding in search.ml some substrings such
 as "_admitted" or "_subproof" we don't want to see in results
 of SearchAbout and co, we now have a user command:

  Add Search Blacklist "foo".
  Remove Search Blacklist "foo". (* the opposite *)
  Print Table Search Blacklist. (* the current state *)

 In Prelude.v, three substrings are blacklisted originally:
  - "_admitted" for internal lemmas due to admit.
  - "_subproof" for internal lemmas due to abstract.
  - "Private_" for hiding auxiliary modules not meant for
    global usage.

 Note that substrings are searched in the fully qualified names
 of the available lemmas (e.g. "Coq.Init.Peano.plus").

 This commit also adds the prefix "Private_" to some internal modules
 in Numbers, Z, N, etc.

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

1 files changed, 2 insertions, 2 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 418fd8e58..30e35f501 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -267,7 +267,7 @@ Include BoolOrderFacts.
     by the generic functor of properties about natural numbers
     instantiated at the end of the file. *)
 
-Module Import BootStrap.
+Module Import Private_BootStrap.
 
 Theorem add_0_r n : n + 0 = n.
 Proof.
@@ -323,7 +323,7 @@ Proof.
  now apply (Pos.add_lt_mono_l p).
 Qed.
 
-End BootStrap.
+End Private_BootStrap.
 
 (** Specification of lt and le. *)