coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Can Type be Set?

From: Tom Prince <tom.prince AT ualberta.net>
To: Adam Chlipala <adam AT chlipala.net>, Gert Smolka <smolka AT ps.uni-saarland.de>
Cc: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Can Type be Set?
Date: Thu, 05 May 2011 12:39:18 -0400

On 2011-05-05, Adam Chlipala wrote:
> Gert Smolka wrote:
> >>> Check (fun X : Type => X) : Set -> Type.
> It looks like something interesting is going on in Coq lately.  I tried
> your original command in Coq 8.2 and got a type error.  Perhaps [Set] is
> truly changed to a synonym for [Type] level 0 in 8.3 and later.

It also fails in trunk.

  Tom

[Coq-Club] Can Type be Set?, Gert Smolka
- Re: [Coq-Club] Can Type be Set?, Adam Chlipala
  - Re: [Coq-Club] Can Type be Set?, Gert Smolka
    - Re: [Coq-Club] Can Type be Set?, Adam Chlipala
      - Re: [Coq-Club] Can Type be Set?, Tom Prince