People absolutely use Coq to generate code. I don't know what else is involved.

A few substantiating links from my search results for "coq generating code":

http://coq.inria.fr/V8.1/refman/Reference-Manual021.html

http://research.microsoft.com/en-us/um/people/akenn/coq/LOLA...

http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...