Towards unifying parsing/printing for universe instances and Type's argument.

We consistently use:
- UUnknown: to mean a rigid anonymous universe
  (written Type in instances and Type as a sort)
  [was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
  (written _ in instances and Type@{_} as a sort)
  [was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
  (written id or qualid in instances and Type@{id} or Type@{qualid} or more
   generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)

There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.

There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.

0 files changed, 0 insertions, 0 deletions