How to get the name of a named goal in the coq api

129 views Asked by At

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?

1

There are 1 answers

0
KöniglichePM On

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.