The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Tue, Jun 30, 2015 at 01:01:29AM -0700, Clément Pit--Claudel wrote:
> Hi all,
> 
> Is there a way to print a structured representation of a lemma's
> statement in Coq? Ideally I'd like to get something like (forall ((A
> type) (x A) (y A)) (impl (eq x y) (eq y x))) given the lemma [forall A
> (x y: A), x = y -> y = x].
> 
> * The code in texmacspp.ml also looks promising, but I have no idea
> how to call into it.

Look at stm.mli/print_ast.  What you get in an XML representation of the
AST, eventually annotated with extra info for each notation node
(something like the "format" attribute for example).
Unfortunately not all AST nodes are correctly printed, there are many
TODO items in texmacspp.

I don't think there is a CoqIDE message for calling that.
Adding it would be easy.  An alternative option is to have Coq
systematically feedback the AST (what PIDE based UI's do IIRC).
Such feedback would reach the UI with no extra additional protocol
message, since the feedback one is extensible.

Best,
-- 
Enrico Tassi