1 files changed, 7 insertions, 1 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 449cd0f0f9..927db9e9e6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -37,7 +37,7 @@ let g_map f g =
   if g.graph == g' then g
   else {g with graph=g'}
 
-let make_sprop_cumulative g = {g with sprop_cumulative=true}
+let set_cumulative_sprop b g = {g with sprop_cumulative=b}
 
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
@@ -148,8 +148,14 @@ let enforce_leq_alg u v g =
   assert (check_leq g u v);
   cg
 
+module Bound =
+struct
+  type t = Prop | Set
+end
+
 exception AlreadyDeclared = G.AlreadyDeclared
 let add_universe u ~lbound ~strict g =
+  let lbound = match lbound with Bound.Prop -> Level.prop | Bound.Set -> Level.set in
   let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
   enforce_constraint (lbound,d,u) {g with graph}