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, 9 insertions, 7 deletions

diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 68f201897..5583142f8 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -79,7 +79,7 @@ End GenericMinMax.
 (** ** Consequences of the minimalist interface: facts about [max]. *)
 
 Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
- Module Import T := !MakeOrderTac O.
+ Module Import Private_Tac := !MakeOrderTac O.
 
 (** An alternative caracterisation of [max], equivalent to
     [max_l /\ max_r] *)
@@ -277,8 +277,9 @@ End MaxLogicalProperties.
 
 Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
  Include MaxLogicalProperties O M.
- Import T.
+ Import Private_Tac.
 
+ Module Import Private_Rev.
  Module ORev := TotalOrderRev O.
  Module MRev <: HasMax ORev.
   Definition max x y := M.min y x.
@@ -286,6 +287,7 @@ Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
   Definition max_r x y := M.min_l y x.
  End MRev.
  Module MPRev := MaxLogicalProperties ORev MRev.
+ End Private_Rev.
 
 Instance min_compat : Proper (eq==>eq==>eq) min.
 Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed.
@@ -578,29 +580,29 @@ End UsualMinMaxLogicalProperties.
 Module UsualMinMaxDecProperties
  (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O).
 
- Module P := MinMaxDecProperties O M.
+ Module Import Private_Dec := MinMaxDecProperties O M.
 
  Lemma max_case_strong : forall n m (P:t -> Type),
   (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
- Proof. intros; apply P.max_case_strong; auto. congruence. Defined.
+ Proof. intros; apply max_case_strong; auto. congruence. Defined.
 
  Lemma max_case : forall n m (P:t -> Type),
   P n -> P m -> P (max n m).
  Proof. intros; apply max_case_strong; auto. Defined.
 
  Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
- Proof. exact P.max_dec. Defined.
+ Proof. exact max_dec. Defined.
 
  Lemma min_case_strong : forall n m (P:O.t -> Type),
   (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
- Proof. intros; apply P.min_case_strong; auto. congruence. Defined.
+ Proof. intros; apply min_case_strong; auto. congruence. Defined.
 
  Lemma min_case : forall n m (P:O.t -> Type),
   P n -> P m -> P (min n m).
  Proof. intros. apply min_case_strong; auto. Defined.
 
  Lemma min_dec : forall n m, {min n m = n} + {min n m = m}.
- Proof. exact P.min_dec. Defined.
+ Proof. exact min_dec. Defined.
 
 End UsualMinMaxDecProperties.