The Coq mailing list

[Julien Narboux <Julien.Narboux AT inria.fr>]

> (2) Is there a tool that can export a Coq script to human readable form?
>          I know that there is coqtex, and that's quite good if you want to
>          typeset the theorems without the proofs. However, proofs in Coq are
>          very much a dialogue, and reading the proof script is much like
>          hearing something talking on a phone without hearing the other
>          party. It'd be nice to be able to record the dialogue between both
>          parties.
>
>
>   
Hi,

Concerning you second question.
You may want to use coq_tex with the coq_example env (without star), for 
instance this question of the faq 
(http://coq.inria.fr/doc/faq.html#htoc54) has been typeset using the 
following code in the latex file:

\begin{coq_example}
Goal forall A B:Prop, A->B-> A/\B.
intros.
split.
assumption.
assumption.
Qed.
\end{coq_example}

But in fact, you will get something very long and not very readable, 
another solution would be to write your proofs using the new declarative 
proof language introduced in Coq 8.1 by Pierre Corbineau 
(http://www.cs.ru.nl/~corbinea/mmode.en.html).

Best wishes,

Julien