The Coq mailing list

[Petter Urkedal <paurkedal AT gmail.com>]

I'd like to create an ordered map over a custom datatype.  I defined
an appropriate module Label_ord such that (Label_ord.t : Set).  If I
try to apply it,

  Module Labelling := FMapAVL.Make(Label_ord).
  Definition labelling : Set → Set := Labelling.t.

the last line gives

  Error: The term "λ elt : Set, Labelling.t elt" has type  "Set →
Type" while it is expected to have type "Set → Set".

I can see from FMapInterface that its t is Type → Type, which I hoped
was universe polymorphic.  I guess the functor coerces the argument's
t component to Type?

Does the Coq-8.4 standard library provide a way to create ordered maps in Set?