First-Class Containers in Coq

We present a Coq library for finite sets and maps which brings the same functional- ities as the existing standardFSets/FMapslibrary, but ensures the genericity of the proposed data structures using type classes instead of modules. This architecture facilitates the use of these data structures thanks to overloading and implicit instantiation, and more generally sim- plifies the implementation of complex algorithms in Coq. It also provides facilities for dealing with ordered types and automatically generating comparison function for structured types.