aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/NatInt
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-08-11 17:03:35 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-08-11 17:03:35 +0000
commite44ffa03378eec03425ec8a2698365f95d7dcb81 (patch)
treeb22329a614dbb622e2e10262d4b5a9641c3b6eb9 /theories/Numbers/NatInt
parent9221176c38519e17522104f5adbbec3fcf755dd4 (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/NatInt')
-rw-r--r--theories/Numbers/NatInt/NZOrder.v10
1 files changed, 6 insertions, 4 deletions
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]. *)