The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I would like to take a coq file, and split it apart into separate files (or strings of code), each of which is a single definition/lemma/notation/hint/etc.  For example, in a file with no sections and no local things, I would like to be able to split it apart into files a.v, b.v which has [Require Export a.], c.v which has [Require Export b.], etc, such that the last file is equivalent to the file I started with.  Equivalently, I would like a program which can take in a .v file, and split the file into a list of chunks [a, b, c, ...], so that if I had loaded the original file into CoqIDE, clicking the "evaluate next" button once would evaluate a, clicking it again would evaluate b, etc.

Is there a good way to do this from bash, python, C, or some other language?

(I'm about to go source-dive CoqIDE and/or ProofGeneral, but I figured I'd ask here first to see if anyone could help me.)

Thanks,

Jason