[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.

0 files changed, 0 insertions, 0 deletions