From e44ffa03378eec03425ec8a2698365f95d7dcb81 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 11 Aug 2011 17:03:35 +0000
Subject: 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
---
 theories/Numbers/Integer/Abstract/ZDivEucl.v  | 2 +-
 theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +-
 theories/Numbers/Integer/Abstract/ZDivTrunc.v | 3 ++-
 3 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'theories/Numbers/Integer/Abstract')

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 954b89150a..fe951a7511 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 0e54c453b7..14003d8926 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 74abedb423..bd8b6ce239 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
-- 
cgit v1.2.3