我目前正在开发一个 ocaml 程序,该程序将使用 coq api 来提取有关证明及其目标的信息。为此,当使用“refine ?[name]”或其他命名目标的策略时,我想提取给目标的名称。到目前为止,我正在获得当前的目标,使用我当前的证明状态来提取它们,如下所示
(*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
...
使用这种方法,我可以提取目标的 ID,但不能提取它们的名称。
有没有可能提取名称?