The Coq mailing list

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

On 06/09/2017 01:14, Jan-Oliver Kaiser wrote:
> Hey everyone,
> 
> List.tl and List.repeat are outliers in the List module as they
> introduce new universes which upper-bound list's own universe variable
> in the global graph. Why is that?

Good catch. They are created because of the implicit argument of nil,
which is of type Type. I have no idea whether this deficiency of Coq is
easily fixed, but we can at least remove these superfluous universes by
explicit setting the argument of nil in the definitions of tl and repeat.

Best regards,

Guillaume