The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

For the record, Pierre Letouzey (main author of the FSets/FMaps
library with Jean-Christophe Filliâtre) has precisely updated last
week his "M" version of FMaps (https://github.com/letouzey/coq-mmaps),
with the plan to release it soon as an opam package.

Best,

Hugo

On Thu, May 14, 2020 at 12:46:38PM -0400, Andrew Appel wrote:
> The MSets interface of the Coq standard library factors the program from the
> proof, and may solve the problem that's being discussed here.
> It was intended as a replacement for FSets and FMaps.
> There had been a plan to make MMaps also (finite maps instead of sets), but
> unfortunately I don't think that was ever done.
> 
> There are efficient implementations of MSets for AVL trees and Red-Black 
> trees
> in the standard library.
>