Expose set interface to option tables

This lets us avoid having to cache the SearchBlacklist.elements call
in search as we can just use the set module's for_all function.

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