aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/names.ml1
-rw-r--r--kernel/names.mli1
-rw-r--r--library/goptions.ml19
-rw-r--r--library/goptions.mli28
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/detyping.mli2
-rw-r--r--vernac/search.ml14
8 files changed, 31 insertions, 38 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 047a1d6525..39cd4548f5 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -671,6 +671,7 @@ module InductiveOrdered_env = struct
let compare = ind_user_ord
end
+module Indset = Set.Make(InductiveOrdered)
module Indmap = Map.Make(InductiveOrdered)
module Indmap_env = Map.Make(InductiveOrdered_env)
diff --git a/kernel/names.mli b/kernel/names.mli
index 2238e932b0..e48cdf26ec 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -481,6 +481,7 @@ type constructor = inductive (* designates the inductive type *)
* int (* the index of the constructor
BEWARE: indexing starts from 1. *)
+module Indset : CSig.SetS with type elt = inductive
module Indmap : CSig.MapS with type key = inductive
module Constrmap : CSig.MapS with type key = constructor
module Indmap_env : CSig.MapS with type key = inductive
diff --git a/library/goptions.ml b/library/goptions.ml
index f4b8ce9465..2798c21c81 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -53,9 +53,9 @@ module MakeTable =
functor
(A : sig
type t
- type key
- val compare : t -> t -> int
- val table : (string * key table_of_A) list ref
+ type key
+ module Set : CSig.SetS with type elt = t
+ val table : (string * key table_of_A) list ref
val encode : Environ.env -> key -> t
val subst : substitution -> t -> t
val printer : t -> Pp.t
@@ -74,7 +74,7 @@ module MakeTable =
if String.List.mem_assoc nick !A.table then
user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.")
- module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
+ module MySet = A.Set
let t = Summary.ref MySet.empty ~name:nick
@@ -119,8 +119,9 @@ module MakeTable =
}
let _ = A.table := (nick, table_of_A)::!A.table
- let active c = MySet.mem c !t
- let elements () = MySet.elements !t
+
+ let v () = !t
+ let active x = A.Set.mem x !t
end
let string_table = ref []
@@ -138,7 +139,7 @@ module StringConvert = functor (A : StringConvertArg) ->
struct
type t = string
type key = string
- let compare = String.compare
+ module Set = CString.Set
let table = string_table
let encode _env x = x
let subst _ x = x
@@ -158,7 +159,7 @@ let get_ref_table k = String.List.assoc (nickname k) !ref_table
module type RefConvertArg =
sig
type t
- val compare : t -> t -> int
+ module Set : CSig.SetS with type elt = t
val encode : Environ.env -> qualid -> t
val subst : substitution -> t -> t
val printer : t -> Pp.t
@@ -171,7 +172,7 @@ module RefConvert = functor (A : RefConvertArg) ->
struct
type t = A.t
type key = qualid
- let compare = A.compare
+ module Set = A.Set
let table = ref_table
let encode = A.encode
let subst = A.subst
diff --git a/library/goptions.mli b/library/goptions.mli
index 381ba4d34a..ba86cb66ba 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -70,8 +70,8 @@ module MakeStringTable :
val member_message : string -> bool -> Pp.t
end) ->
sig
+ val v : unit -> CString.Set.t
val active : string -> bool
- val elements : unit -> string list
end
(** The functor [MakeRefTable] declares a new table of objects of type
@@ -87,19 +87,19 @@ end
module MakeRefTable :
functor
(A : sig
- type t
- val compare : t -> t -> int
- val encode : Environ.env -> qualid -> t
- val subst : substitution -> t -> t
- val printer : t -> Pp.t
- val key : option_name
- val title : string
- val member_message : t -> bool -> Pp.t
- end) ->
- sig
- val active : A.t -> bool
- val elements : unit -> A.t list
- end
+ type t
+ module Set : CSig.SetS with type elt = t
+ val encode : Environ.env -> qualid -> t
+ val subst : substitution -> t -> t
+ val printer : t -> Pp.t
+ val key : option_name
+ val title : string
+ val member_message : t -> bool -> Pp.t
+ end) ->
+sig
+ val v : unit -> A.Set.t
+ val active : A.t -> bool
+end
(** {6 Options. } *)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 90ce1cc594..70a9784238 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -441,7 +441,7 @@ let coercion_of_reference r =
module CoercionPrinting =
struct
type t = coe_typ
- let compare = GlobRef.Ordered.compare
+ module Set = GlobRef.Set
let encode _env = coercion_of_reference
let subst = subst_coe_typ
let printer x = Nametab.pr_global_env Id.Set.empty x
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 82726eccf0..505dc529cf 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -182,7 +182,7 @@ module PrintingInductiveMake =
end) ->
struct
type t = inductive
- let compare = ind_ord
+ module Set = Indset
let encode = Test.encode
let subst subst obj = subst_ind subst obj
let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 00b0578a52..af2baa9713 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -91,7 +91,7 @@ module PrintingInductiveMake :
end) ->
sig
type t = Names.inductive
- val compare : t -> t -> int
+ module Set = Indset
val encode : Environ.env -> Libnames.qualid -> Names.inductive
val subst : substitution -> t -> t
val printer : t -> Pp.t
diff --git a/vernac/search.ml b/vernac/search.ml
index a5663d65ef..2e3a95bed2 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -200,12 +200,10 @@ let full_name_of_reference ref =
DirPath.to_string dir ^ "." ^ Id.to_string id
(** Whether a reference is blacklisted *)
-let blacklist_filter_aux () =
- let l = SearchBlacklist.elements () in
- fun ref env typ ->
+let blacklist_filter ref env typ =
let name = full_name_of_reference ref in
let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
- List.for_all is_not_bl l
+ CString.Set.for_all is_not_bl (SearchBlacklist.v ())
let module_filter (mods, outside) ref env typ =
let sp = Nametab.path_of_global ref in
@@ -227,7 +225,6 @@ let search_about_filter query gr env typ = match query with
(** SearchPattern *)
let search_pattern ?pstate gopt pat mods pr_search =
- let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
@@ -251,7 +248,6 @@ let rewrite_pat2 pat =
let search_rewrite ?pstate gopt pat mods pr_search =
let pat1 = rewrite_pat1 pat in
let pat2 = rewrite_pat2 pat in
- let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
(pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) ||
@@ -266,7 +262,6 @@ let search_rewrite ?pstate gopt pat mods pr_search =
(** Search *)
let search_by_head ?pstate gopt pat mods pr_search =
- let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
@@ -280,7 +275,6 @@ let search_by_head ?pstate gopt pat mods pr_search =
(** SearchAbout *)
let search_about ?pstate gopt items mods pr_search =
- let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
let eqb b1 b2 = if b1 then b2 else not b2 in
module_filter mods ref env typ &&
@@ -324,7 +318,6 @@ let interface_search ?pstate =
let (name, tpe, subtpe, mods, blacklist) =
extract_flags [] [] [] [] false flags
in
- let blacklist_filter = blacklist_filter_aux () in
let filter_function ref env constr =
let id = Names.Id.to_string (Nametab.basename_of_global ref) in
let path = Libnames.dirpath (Nametab.path_of_global ref) in
@@ -378,6 +371,3 @@ let interface_search ?pstate =
in
let () = generic_search ?pstate glnum iter in
!ans
-
-let blacklist_filter ref env typ =
- blacklist_filter_aux () ref env typ
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:34:23 +0000