The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

tumenjargal tsagaan wrote:
> I wanted to rewrite coq-code in a sequence form.
> Is there any automated tool for this purpose?
>
> even better is it if possible in a tex format.

Since there was another very similar question recently, it seems like it 
might be worth making the following point: It's far from clear to me 
that the full generality of Coq proof terms can be represented nicely in 
natural deduction form, or in any other form that most people are going 
to want to read.  Tactics aren't generally generating proof terms with 
an eye toward readability, and many subtle aspects of the underlying 
logic don't match up well with informal mathematical practice.

All this is to say that it's not obvious how such a tool would work; 
it's not just a matter of no one having bothered to implement a clear 
specification yet.  You would almost certainly need to target a 
particular domain of proofs to get good results.