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/ZArith | |
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/ZArith')
-rw-r--r-- | theories/ZArith/BinInt.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 *) |