-type universe = (bool * NUri.uri) list
- (* Max of non-empty list of named universes, or their successor (when true) *)
+type univ_algebra = [ `Type | `Succ | `CProp ]
+
+type universe = (univ_algebra * NUri.uri) list
+ (* Max of non-empty list of named universes, or their successor (when true)
+ * The empty list represents type0 *)