The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

----- Mail original -----
> Hello,
> 
> I need to use a library which depends on the Container library
> developed
> by Stéphane Lescuyer. I saw in the Changelog from Coq 8.3 to Coq 8.4
> beta the following:
> "MSets library: an important evolution of the FSets library.
>   "MSets" stands for Modular (Finite) Sets, by contrast with a
>   forthcoming
>   library of Class (Finite) Sets contributed by S. Lescuyer which
>   will be
>   integrated with the next release of Coq."
> 
> I have two questions about this.
> - Is this the same library as the Containers one?
> (http://coq.inria.fr/pylons/contribs/view/Containers/v8.3)[1]
> - Is integration in Coq still planned? (I didn't see it in the
> Changlog
> so I get it hasn't happened yet.)
> 
> Thanks a lot,
> 
> Alan
> 

Hi Alan.

Indeed, I'm still planning to work someday on the inclusion of Containers
(or a evolution of it) alongside MSets in the standard library. I hope to
be able to share actual implementations (such as AVL) between the two,
with the vision that Modular MSets would then be the static version of Class
Sets (currently Containers). But my preliminary attempts of code sharing ended
up with some universe inconsistencies I still have to investigate.
Anyway, since I started speaking of all this a few years ago, I won't dare
giving a ETA, even an approximative one, sorry. 

Best regards,
Pierre Letouzey