The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

I've been searching the Coq standard library and have been unable to 
find a functor that creates an OrderedType given an FSet or even a List 
of OrderedTypes.  This seems relatively straightforward given the 
implementation of PairOrderedType, so I've probably missed it.  I'd 
rather not duplicate effort, so I thought I'd ask first.

Scott Doerrie