The Coq mailing list

[Stefano Zacchiroli <zack AT bononia.it>]

On Fri, Feb 18, 2005 at 08:36:33PM -0500, Yevgeniy Makarov wrote:
> displayed by Print command, but I am wondering if there is a still
> easier way, namely, if I can get an access to the proof term's inner
> representation.

Is it ok for you to parse XML? If this is the case you can use the Coq
exportation module, have a look at chapter 13.5 of the user manual:
"Exporting Coq theories to XML".

Cheers.

-- 
Stefano Zacchiroli -*- Computer Science PhD student @ Uny Bologna, Italy
zack@{cs.unibo.it,debian.org,bononia.it}
 -%- http://www.bononia.it/zack/
If there's any real truth it's that the entire multidimensional infinity
of the Universe is almost certainly being run by a bunch of maniacs. -!-