[api] Move universe syntax to `Glob_term`

We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.

Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.

This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.

1 files changed, 19 insertions, 0 deletions

diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 3c3f75a68..6ecb479e6 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -22,6 +22,25 @@ open Misctypes
 
 type existential_name = Id.t
 
+(** Sorts *)
+
+type 'a glob_sort_gen =
+  | GProp (** representation of [Prop] literal *)
+  | GSet  (** representation of [Set] literal *)
+  | GType of 'a (** representation of [Type] literal *)
+
+type 'a universe_kind =
+  | UAnonymous
+  | UUnknown
+  | UNamed of 'a
+
+type level_info = Libnames.reference universe_kind
+type glob_level = level_info glob_sort_gen
+type glob_constraint = glob_level * Univ.constraint_type * glob_level
+
+type sort_info = (Libnames.reference * int) option list
+type glob_sort = sort_info glob_sort_gen
+
 (**  The kind of patterns that occurs in "match ... with ... end"
 
      locs here refers to the ident's location, not whole pat *)