coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Universe Polymorphism?

From: Tom Prince <tom.prince AT ualberta.net>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Universe Polymorphism?
Date: Wed, 25 Jul 2012 22:34:12 -0600

Jason Gross
<jasongross9 AT gmail.com>
writes:

> Was there some other problem with it?

It has been a long time since I looked at this, and I don't have time to
test it now, but vaguely recall that the issue is that partial
application (which is the only type of application) loses the
polymorpism.

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?, Valentin ROBERT, 07/21/2012