3 files changed, 0 insertions, 35 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml
index f500693ce..c705a707f 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -442,7 +442,6 @@ let subst_constant_def sub = function
   | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
 
 (** Local variables and graph *)
-type universe_context = Univ.LSet.t * Univ.constraints 
 
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
diff --git a/checker/univ.ml b/checker/univ.ml
index d8ee5c35e..e2e40ddc9 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -370,8 +370,6 @@ module Level = struct
 
 end
 
-module LSet = Set.Make (Level)
-
 (** Level maps *)
 module LMap = Map.Make (Level)
 
@@ -381,8 +379,6 @@ type universe_level = Level.t
 
 type universe_level_subst_fn = universe_level -> universe_level
 
-type universe_set = LSet.t
-
 (* An algebraic universe [universe] is either a universe variable
    [Level.t] or a formal universe known to be greater than some
    universe variables and strictly greater than some (other) universe
@@ -1066,31 +1062,6 @@ let merge_constraints c g =
 
 type constraints = Constraint.t
 
-module Hconstraint =
-  Hashcons.Make(
-    struct
-      type t = univ_constraint
-      type u = universe_level -> universe_level
-      let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
-      let equal (l1,k,l2) (l1',k',l2') =
-	l1 == l1' && k == k' && l2 == l2'
-      let hash = Hashtbl.hash
-    end)
-
-module Hconstraints =
-  Hashcons.Make(
-    struct
-      type t = constraints
-      type u = univ_constraint -> univ_constraint
-      let hashcons huc s =
-	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
-      let equal s s' =
-	List.for_all2eq (==)
-	  (Constraint.elements s)
-	  (Constraint.elements s')
-      let hash = Hashtbl.hash
-    end)
-
 (** A value with universe constraints. *)
 type 'a constrained = 'a * constraints
 
diff --git a/checker/univ.mli b/checker/univ.mli
index b000a7ba2..b2f2c9c18 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -23,11 +23,6 @@ end
 type universe_level = Level.t
 (** Alias name. *)
 
-(** Sets of universe levels *)
-module LSet : Set.S with type elt = universe_level
-
-type universe_set = LSet.t
-
 module Universe :
 sig
   type t