The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Hi. I'm sorry if this is a redundant question since I just signed up
for the discussion list. Is there any way to make explicit the
indexation of the hierarchy of Type (i.e. the index i in Type(i))
when using Coq?  This would seem to be necessary in order to correctly
fix the meaning of statements dealing with different universes.

Thanks---
Carlos Simpson