The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

It should be straightforward to fork Coq and have it extract Props too; I expect this to be at most a 5-line change (probably more like 1-line).  Alternatively, pass -impredicative-set, and replace all instances of Prop with Set.  Do either of those work?

On Fri, Feb 10, 2017 at 8:22 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

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