The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

In the following example:

File 1 (ex1.v) :

Definition dneg (X:Type) := ((X -> Empty_set) -> Empty_set).


File 2 (ex2.v):

Require Export ex1.
Variable X:Set.
Check (dneg X).
Check ((X -> Empty_set)-> Empty_set).


Coq responds that (dneg X) is in Type while ((X -> Empty_set)-> Empty_set) is 
in Set. This does not look right.

Vladimir.