Automatically generate names for universes.

The names are `uXXX` with `XXX` some number avoiding collision.

Note that there may be some collisions with polymorphic binders, eg
something like

~~~
Set Universe Polymorphism.
Section foo.
  Universe u0.
  Definition bar := Type.
  (* bar@{u0} = Type@{u0} but this isn't the section u0 *)

  Definition baz := Type@{u0}. (* this one is the section u0 *)
  Definition foobar := Eval compute in baz -> Type.
  (* Type@{u0} -> Type@{u0} but these aren't the same u0 *)
~~~
So maybe we should do a nametab lookup too. This is strictly a
printing issue (polymorphic binder names have no other use).

In the monomorphic case names are qualified by the parent definition
so it should be fine (barring module/definition collision but we
already have those).

Note that there are still unnamed universes as they didn't go through
UState (eg schemes).

0 files changed, 0 insertions, 0 deletions