diff --git a/engine/uState.ml b/engine/uState.ml
index 5f8b032d8a29c..0ed4404bdf5c8 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -47,8 +47,8 @@ module QState : sig
 end =
 struct
 
-module QSet = Set.Make(Sorts.QVar)
-module QMap = Map.Make(Sorts.QVar)
+module QSet = Sorts.QVar.Set
+module QMap = Sorts.QVar.Map
 
 type t = {
   qmap : Sorts.Quality.t option QMap.t;
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index e0b3ff8176ea1..e471f6c9a31cb 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -54,11 +54,32 @@ struct
       Printf.sprintf "%sα%d" s q
 
   let raw_pr q = Pp.str (to_string q)
+
+  module Self = struct type nonrec t = t let compare = compare end
+  module Set = CSet.Make(Self)
+  module Map = CMap.Make(Self)
 end
 
 module Quality = struct
   type t = QVar of QVar.t | QProp | QSProp | QType
 
+  let equal a b = match a, b with
+    | QVar a, QVar b -> QVar.equal a b
+    | QProp, QProp | QSProp, QSProp | QType, QType -> true
+    | (QVar _ | QProp | QSProp | QType), _ -> false
+
+  let compare a b = match a, b with
+    | QVar a, QVar b -> QVar.compare a b
+    | QVar _, _ -> -1
+    | _, QVar _ -> 1
+    | QProp, QProp -> 0
+    | QProp, _ -> -1
+    | _, QProp -> 1
+    | QSProp, QSProp -> 0
+    | QSProp, _ -> -1
+    | _, QSProp -> 1
+    | QType, QType -> 0
+
   let pr prv = function
     | QVar v -> prv v
     | QProp -> Pp.str "Prop"
@@ -67,6 +88,10 @@ module Quality = struct
 
   let raw_pr q = pr QVar.raw_pr q
 
+  module Self = struct type nonrec t = t let compare = compare end
+  module Set = CSet.Make(Self)
+  module Map = CMap.Make(Self)
+
 end
 
 type t =
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index dc3e8e134f080..2d88d97b2c720 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -29,6 +29,10 @@ sig
   val raw_pr : t -> Pp.t
   val to_string : t -> string
   (** Debug printing *)
+
+  module Set : CSig.SetS with type elt = t
+
+  module Map : CMap.ExtS with type key = t and module Set := Set
 end
 
 module Quality : sig
@@ -36,9 +40,17 @@ module Quality : sig
     | QVar of QVar.t
     | QProp | QSProp | QType
 
+  val equal : t -> t -> bool
+
+  val compare : t -> t -> int
+
   val pr : (QVar.t -> Pp.t) -> t -> Pp.t
 
   val raw_pr : t -> Pp.t
+
+  module Set : CSig.SetS with type elt = t
+
+  module Map : CMap.ExtS with type key = t and module Set := Set
 end
 
 type t = private