aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--theories/Init/Prelude.v4
-rw-r--r--theories/NArith/BinNat.v4
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivEucl.v2
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivFloor.v2
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivTrunc.v3
-rw-r--r--theories/Numbers/NatInt/NZOrder.v10
-rw-r--r--theories/Numbers/Natural/Abstract/NDiv.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NLog.v4
-rw-r--r--theories/Numbers/Natural/Abstract/NPow.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NSqrt.v4
-rw-r--r--theories/Structures/GenericMinMax.v16
-rw-r--r--theories/ZArith/BinInt.v4
-rw-r--r--toplevel/search.ml29
13 files changed, 54 insertions, 32 deletions
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index f9c758054..e929c561c 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -22,4 +22,6 @@ Declare ML Module "ground_plugin".
Declare ML Module "dp_plugin".
Declare ML Module "recdef_plugin".
Declare ML Module "subtac_plugin".
-Declare ML Module "xml_plugin". \ No newline at end of file
+Declare ML Module "xml_plugin".
+(* Default substrings not considered by queries like SearchAbout *)
+Add Search Blacklist "_admitted" "_subproof" "Private_".
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. *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 954b89150..fe951a751 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 0e54c453b..14003d892 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 74abedb42..bd8b6ce23 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
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]. *)
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.
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 68f201897..5583142f8 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -79,7 +79,7 @@ End GenericMinMax.
(** ** Consequences of the minimalist interface: facts about [max]. *)
Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
- Module Import T := !MakeOrderTac O.
+ Module Import Private_Tac := !MakeOrderTac O.
(** An alternative caracterisation of [max], equivalent to
[max_l /\ max_r] *)
@@ -277,8 +277,9 @@ End MaxLogicalProperties.
Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
Include MaxLogicalProperties O M.
- Import T.
+ Import Private_Tac.
+ Module Import Private_Rev.
Module ORev := TotalOrderRev O.
Module MRev <: HasMax ORev.
Definition max x y := M.min y x.
@@ -286,6 +287,7 @@ Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
Definition max_r x y := M.min_l y x.
End MRev.
Module MPRev := MaxLogicalProperties ORev MRev.
+ End Private_Rev.
Instance min_compat : Proper (eq==>eq==>eq) min.
Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed.
@@ -578,29 +580,29 @@ End UsualMinMaxLogicalProperties.
Module UsualMinMaxDecProperties
(Import O:UsualOrderedTypeFull')(Import M:HasMinMax O).
- Module P := MinMaxDecProperties O M.
+ Module Import Private_Dec := MinMaxDecProperties O M.
Lemma max_case_strong : forall n m (P:t -> Type),
(m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
- Proof. intros; apply P.max_case_strong; auto. congruence. Defined.
+ Proof. intros; apply max_case_strong; auto. congruence. Defined.
Lemma max_case : forall n m (P:t -> Type),
P n -> P m -> P (max n m).
Proof. intros; apply max_case_strong; auto. Defined.
Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
- Proof. exact P.max_dec. Defined.
+ Proof. exact max_dec. Defined.
Lemma min_case_strong : forall n m (P:O.t -> Type),
(n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
- Proof. intros; apply P.min_case_strong; auto. congruence. Defined.
+ Proof. intros; apply min_case_strong; auto. congruence. Defined.
Lemma min_case : forall n m (P:O.t -> Type),
P n -> P m -> P (min n m).
Proof. intros. apply min_case_strong; auto. Defined.
Lemma min_dec : forall n m, {min n m = n} + {min n m = m}.
- Proof. exact P.min_dec. Defined.
+ Proof. exact min_dec. Defined.
End UsualMinMaxDecProperties.
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 *)
diff --git a/toplevel/search.ml b/toplevel/search.ml
index a22d5ebc7..7b5d770d2 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -22,6 +22,16 @@ open Printer
open Libnames
open Nametab
+module SearchBlacklist =
+ Goptions.MakeStringTable
+ (struct
+ let key = ["Search";"Blacklist"]
+ let title = "Current search blacklist : "
+ let member_message s b =
+ str ("Search blacklist does "^(if b then "" else "not ")^"include "^s)
+ let synchronous = true
+ end)
+
(* The functions print_constructors and crible implement the behavior needed
for the Coq searching commands.
These functions take as first argument the procedure
@@ -164,6 +174,10 @@ let raw_search_by_head extra_filter display_function pattern =
let name_of_reference ref = string_of_id (basename_of_global ref)
+let full_name_of_reference ref =
+ let (dir,id) = repr_path (path_of_global ref) in
+ string_of_dirpath dir ^ "." ^ string_of_id id
+
(*
* functions to use the new Libtypes facility
*)
@@ -190,20 +204,21 @@ let filter_by_module_from_list = function
| [], _ -> (fun _ _ _ -> true)
| l, outside -> filter_by_module l (not outside)
-let filter_subproof gr _ _ =
- not (string_string_contains ~where:(name_of_reference gr) ~what:"_subproof") &&
- not (string_string_contains ~where:(name_of_reference gr) ~what:"_admitted")
+let filter_blacklist gr _ _ =
+ let name = full_name_of_reference gr in
+ let l = SearchBlacklist.elements () in
+ List.for_all (fun str -> not (string_string_contains ~where:name ~what:str)) l
let (&&&&&) f g x y z = f x y z && g x y z
let search_by_head pat inout =
- text_search_by_head (filter_by_module_from_list inout &&&&& filter_subproof) pat
+ text_search_by_head (filter_by_module_from_list inout &&&&& filter_blacklist) pat
let search_rewrite pat inout =
- text_search_rewrite (filter_by_module_from_list inout &&&&& filter_subproof) pat
+ text_search_rewrite (filter_by_module_from_list inout &&&&& filter_blacklist) pat
let search_pattern pat inout =
- text_pattern_search (filter_by_module_from_list inout &&&&& filter_subproof) pat
+ text_pattern_search (filter_by_module_from_list inout &&&&& filter_blacklist) pat
let gen_filtered_search filter_function display_function =
gen_crible None
@@ -223,7 +238,7 @@ let raw_search_about filter_modules display_function l =
let filter ref' env typ =
filter_modules ref' env typ &&
List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l &&
- filter_subproof ref' () ()
+ filter_blacklist ref' () ()
in
gen_filtered_search filter display_function
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 15:45:19 +0000