Как получить имя названной цели в coq api

Question

В настоящее время я работаю над программой ocaml, которая будет использовать coq api для извлечения информации о доказательствах и их целях. Для этого я хочу извлечь имя, данное цели, когда использовалось "уточнение?[Имя]" или какая-то другая тактика для обозначения цели. На данный момент я получаю текущие цели, используя свое текущее состояние проверки, чтобы извлечь их, как показано ниже.

(*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
...

с помощью этого метода я могу извлекать идентификаторы целей, но не их названия.

Есть ли возможность извлечь имена?

Answer 1

Наконец я нашел способ получить имя названной цели из API. Поскольку, возможно, я не единственный, кому это нужно, я отправляю ответ.

Уже существует функция, которая позволяет печатать название цели в принтере, но, к сожалению, она является частной и не может быть использована. Оно используетNames.Id.print (Termops.evar_suggested_name goal sigma) получить имя, где цель имеет тип Goal.goal и сигма типа Evd.evar_map.