Inserting PPX annotations into extracted OCaml

There are PPX macros in OCaml that derive json conversions, pretty printers, etc. for datatypes. So if you write something liketype bool = true | false [@@deriving yojson] you get a pair of JSON conversion functions bool_to_json and bool_of_yojson. Is there a way to insert these annotations on Coq datatypes during extraction?

(This old issue looks like it may be related. https://github.com/coq/coq/issues/5106)

Using ppx_import as a workaround. https://github.com/ocaml-ppx/ppx_import
For each extracted type you can write type t = [%import:ExtractedModule.t] [@@deriving yojson] and it lets you redefine the type. Obviously ugly but it works and avoids repeating the contents of the definition.

Coq supports attributes, so actually it would not be very hard to do a PR for extraction to actually understand OCaml attributes directly; using ppx_import is very easy tho, so I’m not sure that’d be worth it.