Any good resources on extracting Coq to other languages?

Developing plugins
1

I’m curious as to whether there are any digestable resources on how to extract Coq (or any other theorem prover) into another language. What are you recommendations?