Dear Coq developers,

I am working on a Coq plugin that shall be able to extract information about a proof programmatically, i.e. via OCaml.

More specifically, I would like to extract all closed and aborted goals, used tactics and the hypotheses (the environment) for each of the goals…

I already crawled through the source code of Coq 8.9 which I develop against. In the proof.mli file, I found some information which did not help me as I am not sure if the defined structures give me the information I need.

Can you give me some hint about how to get the following information:

- all open, closed and aborted goals in a proof
- the current list of hypotheses for each of those goals
- the tactics that led to the goals

As I want to do it myself, I would be grateful for just the information which data structures and functions can/should be used to fetch the information.

Regards

Mario