The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Sun, Sep 12, 2010 at 10:24:24AM -0400, Jim Apple wrote:
> In the 8.3rc1 sources, MSetAVL.v refers the reader MSetFullAVL for
> proofs of the balance conditions and for non-structually-recursive
> functions for a few operations, but MSetFullAVL.v is not in
> theories/MSets.
> 
> Doe anyone know where I might find MSetFullAVL.v? I did find
> FMapFullAVL.v in theories/FSets.
> 
> Jim


Hi Jim,

MSet is still work-in-progress, even if the existing files are
already usable. For instance, I still have to update maps via the same
recipes. Concerning MSetFullAVL, it seems indeed that I forgot to
create it out of FSetFullAVL. You can find this FSetFullAVL in
user's contrib Orsay/FSets (see [1]): at some point, we decided that
this rather heavy file isn't so useful for the average user. In
particular, we "morally" know that the set operators in FSetAVL
preserve balancing, since the same code is proved in FSetFullAVL.
MSetFullAVL was not seen as a priority since the set operator code
in MSetAVL is directly reused from FSetAVL. Btw, an interesting point
is that improvements in the module system (the Include feature)
will now allow to share code between Full and non-Full version.
I'll let you know when such a MSetFullAVL is ready.

Best regards,

Pierre Letouzey

[1] 
https://gforge.inria.fr/scm/viewvc.php/trunk/Orsay/FSets/?root=coq-contribs