| Age | Commit message (Collapse) | Author |
|---|
|
There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
|
|
|
|
|
|
Instead of looking into the name-oriented structure we look into the
actual section structures.
Note: together with #8475 this lets us remove UnivNames.add_global_universe.
|
|
This is the only information we care about. The printing mechanism is only
called on polymorphic constants, as the naming of global monomorphic levels
is performed in another module.
|
|
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
|
|
|
This API is a bit strange, I expect it will change at some point.
|
