The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 06/09/2017 10:42, Jacques-Henri Jourdan wrote:
> My naive understanding is that it would create a fresh (set of) universe
> variable, and copy all the edges of the existing universe variable of
> the list inductive type. But there should not be any direct constraint
> between the fresh universe to the one of the original list definition.

I don't think it has ever worked that way. (That said, I never
understood why it was called "template", so maybe it was meant to work
that way). For instance, if you type

  Check (fun T : Type => list T).

you get a constraint between the Type type here and the one from the
definition of list:

  Top.1 |= Top.1 <= Coq.Init.Datatypes.44

Best regards,

Guillaume