Moved the text about exporting Coq code to Introduction