The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Maybe try removing " | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)" from flag_of_type in https://github.com/coq/coq/blob/trunk/plugins/extraction/extraction.ml?  Also maybe look at removing instances of Kill kProp in that file?

On Fri, Feb 10, 2017, 9:03 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

Possibly. JSON is an acceptable format. I'm not familiar with the Coq internals; do you know where I would look to make such a change?

On Sat, Feb 11, 2017 at 2:32 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

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