Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.

Reviewed-by: SkySkimmer

1 files changed, 6 insertions, 0 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5f5f0ef8cd..927db9e9e6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -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}