The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Hi,

On 09/02/2015 10:57, Arnaud Spiwack wrote:
> On 6 February 2015 at 14:57, Strub, Pierre-Yves 
> <pierre-yves AT strub.nu
> <mailto:pierre-yves AT strub.nu>>
>  wrote:
> 
>     One of the two must be that one, that I wrote after the third time
>     somebody asked me "How would you do finite sets over an infinite
>     carrier in ssr". This is not something I'm planing to maintain anyway.
> 
>     https://github.com/strub/ssrmisc/blob/master/fset.v
> 
> 
> Indeed, and I don't feel at liberty to say anything more about the other
> one which hasn't been, to the best of my knowledge, publicly announced [...]

It's me, and its a finite set and finite map library, that used to be
based on prior work by Beta Ziliani, which I modified and extended
heavily (the work, not Beta). I also integrated features I saw here and
there in Pierre-Yves' former work and now in what I saw Chistian and
Arnaud sent.

It's still work in progress, and I plan to release it in within a few
weeks, and to maintain it.

Best,
-- 
Cyril Cohen