The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi,
I have some basic question about the hierarchy of universes in Coq. 
Suppose that we have the following code fragment:
Definition PT  := Type.
Definition ED : PT := Type.
Definition PD : PT := Type.
Print Universes.
Variable Test : ED->Prop.
Variable x : ED.
Variable y : PD.
Check Test x.
Check Test y.
We expect that the universes ED and PD are different, however, the test 
works for both.
Printing universes confirms that the universes are distinct :
    univ.5 < univ.1
    univ.3 < univ.1
Does anyone have ideas or suggestions?
Thanks in advance,
Richard

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard