I have found:

`Coq.Structures.DecidableType`

and`Coq.Structures.DecidableTypeEx`

(265 lines) in which is written:

```
(** NB: This file is here only for compatibility with earlier version of
[FSets] and [FMap]. Please use [Structures/Equalities.v] directly now. *)
```

`Coq.Fsets`

(15891 lines) : the stdlib doc says "Modular implementation of finite sets/maps using lists or efficient trees. For sets, please consider the more modern MSets. " and coq-community has coq-mmaps which claims "This is an updated version of the Coq Stdlib's FMaps that is meant to complement the Stdlib's MSet library."

Any opinions about these (deprecate? remove? don't do anything?)

(I'm not giving up on Arith, just pointing this before I forget)

lots of people are using FSet/FMap. We are trying to get MMaps into the Coq Platform as a way to get FMap users to migrate to MMaps. I guess deprecation/removal of FSet/FMap can be considered when there is an extensively tested/used alternative

Last updated: Oct 13 2024 at 01:02 UTC