+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 *)
+
+type sort = Prop | Type of universe
+
+type implicit_annotation =
+ [ `Closed | `Type | `Hole | `Tagged of string | `Term | `Typeof of int | `Vector ]