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

12 files changed, 32 insertions, 25 deletions

diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index f9c758054..e929c561c 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -22,4 +22,6 @@ Declare ML Module "ground_plugin".
 Declare ML Module "dp_plugin".
 Declare ML Module "recdef_plugin".
 Declare ML Module "subtac_plugin".
-Declare ML Module "xml_plugin".
\ No newline at end of file
+Declare ML Module "xml_plugin".
+(* Default substrings not considered by queries like SearchAbout *)
+Add Search Blacklist "_admitted" "_subproof" "Private_".
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. *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 954b89150..fe951a751 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -43,7 +43,7 @@ Module ZEuclidProp
  (Import C : ZSgnAbsProp A B)
  (Import D : ZEuclid' A).
 
- Module Import NZDivP := Nop <+ NZDivProp A D B.
+ Module Import Private_NZDiv := Nop <+ NZDivProp A D B.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index 0e54c453b..14003d892 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -32,7 +32,7 @@ Module Type ZDivProp
  (Import C : ZSgnAbsProp A B).
 
 (** We benefit from what already exists for NZ *)
-Module Import NZDivP := Nop <+ NZDivProp A A B.
+Module Import Private_NZDiv := Nop <+ NZDivProp A A B.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 74abedb42..bd8b6ce23 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -33,6 +33,7 @@ Module Type ZQuotProp
 
 (** We benefit from what already exists for NZ *)
 
+ Module Import Private_Div.
  Module Quot2Div <: NZDiv A.
   Definition div := quot.
   Definition modulo := A.rem.
@@ -41,8 +42,8 @@ Module Type ZQuotProp
   Definition div_mod := quot_rem.
   Definition mod_bound_pos := rem_bound_pos.
  End Quot2Div.
-
  Module NZQuot := Nop <+ NZDivProp A Quot2Div B.
+ End Private_Div.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 3722d4727..8cf5b26fb 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -146,7 +146,8 @@ Definition lt_compat := lt_wd.
 Definition lt_total := lt_trichotomy.
 Definition le_lteq := lt_eq_cases.
 
-Module OrderElts <: TotalOrder.
+Module Private_OrderTac.
+Module Elts <: TotalOrder.
  Definition t := t.
  Definition eq := eq.
  Definition lt := lt.
@@ -156,9 +157,10 @@ Module OrderElts <: TotalOrder.
  Definition lt_compat := lt_compat.
  Definition lt_total := lt_total.
  Definition le_lteq := le_lteq.
-End OrderElts.
-Module OrderTac := !MakeOrderTac OrderElts.
-Ltac order := OrderTac.order.
+End Elts.
+Module Tac := !MakeOrderTac Elts.
+End Private_OrderTac.
+Ltac order := Private_OrderTac.Tac.order.
 
 (** Some direct consequences of [order]. *)
 
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 105051611..6db8e4489 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -13,7 +13,7 @@ Require Import NAxioms NSub NZDiv.
 Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
 
 (** We benefit from what already exists for NZ *)
-Module Import NZDivP := Nop <+ NZDivProp N N NP.
+Module Import Private_NZDiv := Nop <+ NZDivProp N N NP.
 
 Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l.
 
diff --git a/theories/Numbers/Natural/Abstract/NLog.v b/theories/Numbers/Natural/Abstract/NLog.v
index 0accf38b0..74827c6e7 100644
--- a/theories/Numbers/Natural/Abstract/NLog.v
+++ b/theories/Numbers/Natural/Abstract/NLog.v
@@ -18,6 +18,6 @@ Module Type NLog2Prop
 
  (** For the moment we simply reuse NZ properties *)
 
- Include NZLog2Prop A A A B D.NZPowP.
- Include NZLog2UpProp A A A B D.NZPowP.
+ Include NZLog2Prop A A A B D.Private_NZPow.
+ Include NZLog2UpProp A A A B D.Private_NZPow.
 End NLog2Prop.
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index b046e383d..07aee9c6f 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -17,7 +17,7 @@ Module Type NPowProp
  (Import B : NSubProp A)
  (Import C : NParityProp A B).
 
- Module Import NZPowP := Nop <+ NZPowProp A A B.
+ Module Import Private_NZPow := Nop <+ NZPowProp A A B.
 
 Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
 Ltac wrap l := intros; apply l; auto'.
diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
index 1b49678e4..34b7d0110 100644
--- a/theories/Numbers/Natural/Abstract/NSqrt.v
+++ b/theories/Numbers/Natural/Abstract/NSqrt.v
@@ -12,7 +12,7 @@ Require Import NAxioms NSub NZSqrt.
 
 Module NSqrtProp (Import A : NAxiomsSig')(Import B : NSubProp A).
 
- Module Import NZSqrtP := Nop <+ NZSqrtProp A A B.
+ Module Import Private_NZSqrt := Nop <+ NZSqrtProp A A B.
 
  Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
  Ltac wrap l := intros; apply l; auto'.
@@ -70,6 +70,6 @@ Proof. wrap add_sqrt_le. Qed.
 
 (** For the moment, we include stuff about [sqrt_up] with patching them. *)
 
-Include NZSqrtUpProp A A B NZSqrtP.
+Include NZSqrtUpProp A A B Private_NZSqrt.
 
 End NSqrtProp.
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.
 
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index ad1aefaf1..3a5eb8855 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -207,7 +207,7 @@ Qed.
   to prove specifications of operations, but will also be provided
   later by the generic functor of properties. *)
 
-Module Import BootStrap.
+Module Import Private_BootStrap.
 
 (** * Properties of addition *)
 
@@ -374,7 +374,7 @@ Proof.
  rewrite !(mul_comm _ p). apply mul_add_distr_l.
 Qed.
 
-End BootStrap.
+End Private_BootStrap.
 
 (** * Proofs of specifications *)