diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-11 17:03:35 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-11 17:03:35 +0000 |
commit | e44ffa03378eec03425ec8a2698365f95d7dcb81 (patch) | |
tree | b22329a614dbb622e2e10262d4b5a9641c3b6eb9 /theories/Numbers/Natural | |
parent | 9221176c38519e17522104f5adbbec3fcf755dd4 (diff) |
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
Diffstat (limited to 'theories/Numbers/Natural')
-rw-r--r-- | theories/Numbers/Natural/Abstract/NDiv.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NLog.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NPow.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NSqrt.v | 4 |
4 files changed, 6 insertions, 6 deletions
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. |