The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

The toplevel variables are not usually fixed but flexible (akin to
unification variable, although their state evolve by comparison
constraints rather than unification only). Top.14 and Top.8 denote
such variables that are not fully-determined yet. They contain the
name Top because you test from the toplevel; put this code in Foo.v
and you'll see something like Foo.3 and Foo.4 instead.

(I agree that "Top" is somewhat confusing as one thinks first of the
top element of a lattice. It's just the toplevel.)

On Thu, Jan 22, 2015 at 8:39 AM, Kirill Taran 
<kirill.t256 AT gmail.com>
 wrote:
> Hello,
>
> I am playing with "Set Printing Universes". Some types has universe level
> like "Top.14" or "Top.8". What does it mean? Is it fixed level or variable?
>
> For instance,
>     Set Printing Universes.
>     Record Category : Type := {
>       Ob : Type;
>       Hom : Ob -> Ob -> Type
>     }.
>     Check Category.
> gives output:
>     Category : Type (* max ((Top.14)+1, (Top.15)+1) *)
>
> Sincerely,
> Kirill Taran