Como gerar um pdf a partir de um arquivo do Coq?

Existem diversas maneiras de gerar um pdf a partir de um arquivo do Coq. Assumimos que você tem o \LaTeX instalado no seu computador.

1. Crie um diretório contendo um arquivo inicial do \LaTeX, digamos relatorio.tex (um exemplo encontra-se disponível em http://flaviomoura.info/files/relatorio.tex); o arquivo de configuração coqdoc.sty (disponível em http://flaviomoura.info/files/coqdoc.sty); e o seu arquivo do Coq, digamos fileCoq.v.
2. Digite em um terminal (no diretório que contém o arquivo Coq): coqdoc –latex –body-only -s fileCoq.v
3. Em seguida, digite: pdflatex relatorio.tex
4. Abra o arquivo relatorio.pdf com o aplicativo de sua preferência.
5. Para mais informações sobre o CoqDoc, consulte https://coq.inria.fr/refman/using/tools/coqdoc.html