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/NArith/BinNat.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/NArith') 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. *) -- cgit v1.2.3