2 files changed, 12 insertions, 5 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 86aebbce93..d3201bcb9d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1879,11 +1879,17 @@ struct
   let diff (univs, cst) (univs', cst') =
     LSet.diff univs univs', Constraint.diff cst cst'
 
-  let add_constraints (univs, cst) cst' =
+  let add_universe u (univs, cst) =
+    LSet.add u univs, cst
+
+  let add_constraints cst' (univs, cst) =
     univs, Constraint.union cst cst'
 
-  let add_universes univs ctx =
-    union (of_instance univs) ctx
+  let add_instance inst (univs, cst) =
+    let v = Instance.to_array inst in
+    let fold accu u = LSet.add u accu in
+    let univs = Array.fold_left fold univs v in
+    (univs, cst)
 
   let to_context (ctx, cst) =
     (Instance.of_array (Array.of_list (LSet.elements ctx)), cst)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 655f87bb56..3779c055d0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -340,8 +340,9 @@ sig
 
   val union : t -> t -> t
   val diff : t -> t -> t
-  val add_constraints : t -> constraints -> t
-  val add_universes : Instance.t -> t -> t
+  val add_universe : universe_level -> t -> t
+  val add_constraints : constraints -> t -> t
+  val add_instance : Instance.t -> t -> t
 
   (** Arbitrary choice of linear order of the variables *)
   val to_context : t -> universe_context