The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 19/05/2013 01:00, AUGER Cédric wrote:
> Some other interesting stuff for you may be to use the Extraction
> command. It extracts to Ocaml, but the syntax is a lot like Coq's one,
> so you could copy-paste it.

I think you may even tweak the extraction plugin, which only extracts to 
a miniML, to adapt it to the Coq syntax, but it will be quite ugly.

Basing a tactic upon extraction may be a good way to go though.

PMP