Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Universe Polymorphism?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Universe Polymorphism?


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page