I'm currently working on an ocaml program, which will be using the coq api to extract information about proofs and their goals. For this, I want to extract the name given to a goal, when a "refine ?[name]" or some other tactic to name a goal, was used. As of now I am getting the current goals, using my current proof state to extract them like shown below
(*currstate is the current state of the proof*)
let pstate = match currentstate.proof with
| None ->
begin
failwith ""
end
| Some pst -> pst
in
let goals = (Proof.data pstate).goals in
...
with this method I am able to extract the IDs of the goals, but not the name they were given.
Is there any possibility to extract the names?
I finally found a way to retrieve the name of a named goal from the API. Because I may not be the only one looking in need of this, I am posting an answer.
There already exist a function which lets you print the name of a goal in Printer, but sadly it is private and cannot be used. It uses
Names.Id.print (Termops.evar_suggested_name goal sigma)
to retrieve the name, where goal is of typeGoal.goal
and sigma of typeEvd.evar_map
.