Most of the action happens in this file: https://github.com/pirapira/coq2rust/blob/rust/plugins/extraction/rust.ml https://github.com/pirapira/coq2rust/blob/ru

Most of the action happens in this file: https://github.com/pirapira/coq2rust/blob/rust/plugins/extraction/rust.ml https://github.com/pirapira/coq2rust/blob/rust/plugins/extra... I have considered attempting to write a few code extraction plugins for Coq, but I took a long look at the extraction plugin for Scala (https://bitbucket.org/yoshihiro503/coq2scala/src/1657d65c747bb9747a4ec32b3da36464631bcd18/coq-8.3pl2/plugins/extraction/scala.ml?at=master&fileviewer=file-view-default https://bitbucket.org/yoshihiro503/coq2scala/src/1657d65c747...) and lost all courage.