There are PPX macros in OCaml that derive json conversions, pretty printers, etc. for datatypes. So if you write something like
type bool = true | false [@@deriving yojson] you get a pair of JSON conversion functions
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)