I would like to announce the release of Deriving v0.1.0 (GitHub - arthuraa/deriving: Class instances for Coq inductive types with little boilerplate, available as
coq-deriving on OPAM). It is a library for automating the generation of MathComp class instances for inductive types, akin to how
deriving declarations work in OCaml or Haskell. With a few lines of code, you can derive instances of
choiceType, etc. for your types. The instances are defined using the recursion scheme for the types, and they can be generated even for mutually inductive and nested inductive types (provided that you define the recursion scheme yourself). Check the GitHub page for examples!