From 4541d28ba3c50bc8e45c4ccf418bbdd225454dec Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 3 Jun 2019 14:32:18 +0200
Subject: 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.
---
 pretyping/classops.ml  | 2 +-
 pretyping/detyping.ml  | 2 +-
 pretyping/detyping.mli | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3