The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

Hi everyone,

I have a question about sort polymorphism in Coq 8.1.  Consider the  
following example.

(* *** *)

Parameter bind : Set.

Definition env := list.

Print env.         (* env        : Type -> Type *)
Check (env bind).  (* env bind   : Type *)
Check (list bind). (* list bind  : Set *)

(* *** *)

My question: why are (env bind) and (list bind) assigned different  
sorts?  The two are convertible with each other.  It seems strange  
that "wrapping" list behind a Definition would all of a sudden change  
the sorts that are assigned to entities.  What exactly is going on here?

Thanks for any help and clarification,
Brian