The Coq mailing list

[CHA Reeseo <reeseo AT formal.korea.ac.kr>]

2009/7/20 CoqUser CoqUser 
<coquser AT yahoo.com>:
> I need standard proofs trees as on page 123 of the Coq 8.2 Reference Manual
> preferably in latex form not dependency graphs.

On page 123 of Reference Manual[1], I found a bunch of inference (typing)
rules.  For type-setting trees made up of these rules (in LaTeX), I've
usually hand-coded everything using BuffProofs[2] package.

According to the man page[3], coq-tex doesn't seem to be an appropriate
tool for proof TREEs.  It rather seems to be a tool to interact with
coqtop for some snippet of Coq code embedded in LaTeX source.

If you just want to get a hierarchical structure of your proof, the
command "Show Tree" will help[4].

[1] http://coq.inria.fr/distrib/V8.2pl1/files/Reference-Manual.pdf
[2] http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/
[3] http://www.penguin-soft.com/penguin/man/1/coq-tex.html
[4] http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#toc46

-- 
CHA Reeseo
http://www.reeseo.net/