The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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].

* Basic extracting to JSON doesn't do, because Props are erased before 
extraction.
* The PrintAst XML command looks promising, but I'm not sure what its syntax 
is. [1]
* The code in texmacspp.ml also looks promising, but I have no idea how to 
call into it.

Thanks!

[1] More generally, I'm not sure how to invoke the IDE slave mode in trunk: 
the following command works with 8.4pl2, but on trunk it prints "Fatal error: 
ideslave communication channels not set.":
      coqtop -ideslave <<< '<call val="mkcases">nat</call>'