The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

 Dear Yevgeniy,

> written in Scheme). It is quite possible to parse proof terms that are
> 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.

 You can get access to the proof term's inner representation in XML.
 Look at chapter "13.5  Exporting Coq theories to XML" of the Coq manual.
 The XML representation is an encoding of the proof term in the CIC, as it
 is seen by the kernel of Coq (up to very minor variations).

                                        Regards,
                                        C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------