The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Sun, 15 Apr 2007 12:27:11 +0300,
Lauri Alanko 
<la AT iki.fi>
 a écrit :

> Hello. 
> 
> I'm wondering about the prospects of universe polymorphism in Coq. The
> idea has been around for ages, and every now and then someone stumbles
> into a universe inconsistency while trying to do neat self-referential
> tricks, so obviously there would be use for the feature. So is it
> missing from Coq because its implementation would present technical
> (or theoretical) problems, or is it simply not a very high priority
> for the developers?
> 
> I understand that universe inconsistencies come up only in very
> special kinds of situations, but when they do, they are quite
> annoying: one moment you're working on a level of superbly high
> abstractions, the next moment you find that you have to physically
> copy files to get separate, higher-universe instances of crucial
> types...
> 
> Thanks in advance.
> 
> 
> Lauri

I am not sure what you call universe polymorphism, but I think Hugo
Herbelin implemented something in coq 8.1. Could you be more precise
pls?

Cheers,
P.C.