The Coq mailing list

["Edward Z. Yang" <ezyang AT mit.edu>]

Hello Stephane,

Is there a way to access, say, hypotheses in an in-progress proof,
or the goals, and pass them to the Print XML facility?  (Think of:
domain specific proof general application)

Edward

Excerpts from Stéphane Glondu's message of Thu Apr 05 09:09:09 -0400 2012:
> Le 04/04/2012 21:05, Edward Z. Yang a écrit :
> > Is there a nice, easy to parse format for Coq terms (e.g. "or False (or 
> > False
> > (or False (or (((A -> B) -> A) -> A) False)))" or Set Printing All on
> > steroids)?  I am building a parser for a fragment of the Coq term language
> > (since this doesn't involve patching Coq), but it would be much nicer if I
> > could get everything in a nicer format.
> 
> Print XML
> 
> 
> Cheers,
>