The Coq mailing list

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

On Thu, Oct 09, 2014 at 10:02:34AM +0200, Carst Tankink wrote:
> hypotheses, for example) and I expect it would be possible to use the
> functions introduced for printing the AST to also print the statements in
> the goals as XML, but that will take a while to be done, so I have no idea
> if it'll make it into 8.5

IIRC some Coq working groups ago Yann told me he had a patch that makes
the textual pretty printer "predict" the location of the terms.
Today to print a term one goes trough the AST data we can print in XML,
but the locations are dummy.  To recover them, one would need to
re-parse what was just printed.

I have not seen this patch merged, but if it gets in the repo then we
are golden.

WRT Ltac, I think it is possible to print the generic, extensible, AST.
It is just that Francois did not need it.

In any case help is very welcome, the XML pretty printer is not 100%
complete, but is not very hard to contribute to that piece of code.

Best,
-- 
Enrico Tassi