The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hello,

For a project I'm working on, I need to be able to get ASTs for Coq terms. So far I'm aware of a few options:

• JSON extraction in 8.5, which does not work for us because we also need information in Prop
• A Peacoq plugin which we are trying to get working
  
• The XML protocol, which I know nothing about (is this useful?) but see referenced in old Coq-club threads
  
• template-coq, which is neat but does not fit our needs

I'm wondering if anyone knows of any other parsers that produce ASTs for Coq terms, including Props, preferably as s-expressions (or something similarly versatile).

Thanks,

Talia