The Coq code extraction feature produces executable code in conventional functional languages that can be integrated with existing components. Currently, Coq features extraction into OCaml, Haskell and Scheme. Many new target languages are not covered by the standard Coq extraction, such as languages for smart contracts and web development. Moreover, the extraction procedure is written in OCaml and is not verified. Implementing extraction in Coq itself allows for verification of the extraction process. We implement an extraction pipeline by extending the MetaCoq verified erasure with proof-generating passes and verified optimisations. We support several languages from the ML family in our pipeline: two languages for smart contracts (Liquidity and CameLIGO) and the Elm programming language. Our experience shows the pipeline can handle practical use cases and can be extended with more target languages including the ML family.