coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Tom Prince <tom.prince AT ualberta.net>
- To: Jason Gross <jasongross9 AT gmail.com>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Universe Polymorphism?
- Date: Fri, 20 Jul 2012 23:03:40 -0600
Jason Gross
<jasongross9 AT gmail.com>
writes:
> Hi,
> I noticed that Coq seems to have had universe polymorphism at one point,
> but no longer does (see commit message at the bottom of the message). Is
> there somewhere that I can find an explanation of why this was removed, or
> can someone respond with an explanation? (If it was discussed on coq-club
> before, are there archives of coq-club@, and can someone point me to them?)
coq has for a long time had a limited support for universe polymorphism
for inductive types. The commit you reference was an attempt at adding
more support, but it wasn't actually effective (hence the revert).
Tom
- [Coq-Club] Universe Polymorphism?, Jason Gross, 07/21/2012
- Re: [Coq-Club] Universe Polymorphism?, Tom Prince, 07/21/2012
- Re: [Coq-Club] Universe Polymorphism?, Jason Gross, 07/24/2012
- Re: [Coq-Club] Universe Polymorphism?, Tom Prince, 07/26/2012
- Re: [Coq-Club] Universe Polymorphism?, Jason Gross, 07/26/2012
- Re: [Coq-Club] Universe Polymorphism?, Tom Prince, 07/26/2012
- Re: [Coq-Club] Universe Polymorphism?, Jason Gross, 07/24/2012
- Re: [Coq-Club] Universe Polymorphism?, Valentin ROBERT, 07/21/2012
- Re: [Coq-Club] Universe Polymorphism?, Tom Prince, 07/21/2012
Archive powered by MHonArc 2.6.18.