2

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?

KöniglichePM
  • 21
  • 1

1 Answers1

0

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 type Goal.goal and sigma of type Evd.evar_map.

KöniglichePM
  • 21
  • 1