The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

CoqUser CoqUser a écrit :
> Is it possible to generate proof trees formatted like page 123 of Coq 
> v.8.2 Reference Manual directly from Coq proof text files?  The 
> reference manual mentions coq-tex, but there's no documentation.
The trees are described in doc/common/macros.tex in the SVN repository:
\newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}}
\newcommand{\WFE}[1]{\WF{E}{#1}}
\newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}}
\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}

\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
\newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\cal W\!F}(#2)}}
\newcommand{\WS}[3]{\ensuremath{#1[] \vdash #2 <: #3}}
\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra  #3$}}
\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}

\newcommand{\WTRED}[5]{\mbox{$#1[#2] \vdash #3 #4 #5$}}
\newcommand{\WTERED}[4]{\mbox{$E[#1] \vdash #2 #3 #4$}}
\newcommand{\WTELECONV}[3]{\WTERED{#1}{#2}{\leconvert}{#3}}
\newcommand{\WTEGRED}[3]{\WTERED{\Gamma}{#1}{#2}{#3}}
\newcommand{\WTECONV}[3]{\WTERED{#1}{#2}{\convert}{#3}}
\newcommand{\WTEGCONV}[2]{\WTERED{\Gamma}{#1}{\convert}{#2}}
\newcommand{\WTEGLECONV}[2]{\WTERED{\Gamma}{#1}{\leconvert}{#2}}

For coq-tex, take a look at
tools/README.coq-tex
and
tools/coq_tex.ml4
and
man coq-tex
may help

Maybe by hacking coq_tex.ml4, you can produce what you want...

By the way, give a more accurate reference for your page, since on-line 
html refman has no pages on it.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay