I’m working on a project where for various reasons I’ve found myself needing to inspect the intermediate proof contexts of Coq proofs in a programmatic way from OCaml.

**Example:**

```
(* proof.v *)
Lemma add_comm: forall x y, x + y = y + x.
Proof.
intros x; induction x as [| x IHx].
- intros y; induction y; auto.
- intros y.
rewrite plus_Sn_m.
(* [view proof context here] *)
rewrite IHx.
rewrite plus_n_Sm.
auto.
Qed.
```

I’d like to get programatic access to view the corresponding proof context at the marked intermediate point from OCaml:

```
1 goal (ID 22)
x : nat
IHx : forall y : nat, x + y = y + x
y : nat
============================
S (x + y) = y + S x
```

Note: I don’t need to modify/update/change the context, simply access it.

**Naive Solution**

One simple way to do this would be to run coqtop as a external process and feed it in the prefix of the proof, and then use the show tactic and parse the result, but this seems fragile.

**Problem**

Seeing as I’m writing in OCaml anyway, I thought I’d try just running Coq directly as a library, and then reading the proof context directly through Coq’s own API, bypassing the need to do the parsing myself (albeit having to deal directly with the proof terms rather than the simplified notations).

Unfortunately, there isn’t much documentation on exactly which of Coq’s APIs need to be called in which order in order for Coq to be able to load a given file, so I’ve been running into issues with my programs just crashing at runtime when trying to invoke Coq, with fairly esoteric error messages such as “entry [integer] is empty”, etc.

**As such, I’m wondering if anyone could point me to any examples of Coq being used in this way? or some minimal code snippet that I could use as a starting point for doing this?**

or is this more difficult than it’s worth, and it’s probably better to just bite the bullet and parse the proof state instead?