The Coq mailing list

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

Hi,

I have a question about Coq 8.2 (beta), specifically about sort  
polymorphism and the module system.  I'm going to use the FSets  
library as an example.

<<
Require Import FSets.

Module NatSet := FSetWeakList.Make Nat_as_DT.

Print NatSet.elt.  (* NatSet.elt = nat : Type *)
>>

My question: Given the definition of NatSet.elt, I would expect that  
it could be given type Set.  After all, nat has type Set.  However,  
"Check (NatSet.elt : Set)" fails.  Why is this the case?  Judging from  
the description of sort polymorphism in the reference manual, perhaps  
I'm expecting more than is actually the case?

Thank you for help and pointers,
Brian