I'm using Proof.run_tactic
in Coq 8.9, and I would like to get back the new contexts (an env
) and conclusions (a constr
) for each subgoal.
I am able to get a Goal.goal list
, and I am able to use the functions Goal.V82.env
, Goal.V82.concl
, and Goal.V82.abstract_type
.
Goal.V82.env
seems to return nothing.Goal.V82.concl
returns the correct conclusion, but all of the Rel
indices are replaced with Var
s.Goal.V82.abstract_type
returns the conclusion with the correct indices, BUT it is prepended with a Product for every name in the new context. This isn't enough because I can't tell how many products still belong in the new conclusion.Any tips? Thank you!
buuump we'd super love help if anyone knows :). @Emilio Jesús Gallego Arias ?
RanDair does val hyps : t -> EConstr.named_context
get you anything?
I think that would be what maps the vars
have a look around https://github.com/coq/coq/blob/5714656cb3f8a676c126a8d8e67ea2d92781d780/engine/proofview.mli#L517 (8.9 api should be similar)
Goal.V82.env seems to return nothing.
I don't know what you mean by "nothing"
Goal.V82.concl returns the correct conclusion, but all of the Rel indices are replaced with Vars.
Var is correct, I don't know why you expect Rel
I don't even have a 8.9 tree around that works in my current dev workflow sorry @Talia Ringer , I was hesitant to give thus incorrect advice; one thing that may help is to look at the goal printer, there you can see how the different bits of goals are extracted from the proof state, but that API is still a bit in flux (Proof.t
and friends)
Gaëtan Gilbert said:
I don't know what you mean by "nothing"
My bad, I meant that I did not see any indices pushed onto that environment.
Var is correct, I don't know why you expect Rel
I think I expected a Rel because I want to use the goal to call Proof.run_tactic
again with the proper goal and context.
My bad, I meant that I did not see any indices pushed onto that environment.
context variables are in the named_context part of the env
I think I expected a Rel because I want to use the goal to call Proof.run_tactic again with the proper goal and context.
I don't see how the 2 parts of this sentence are connected
Last updated: Jun 09 2023 at 07:01 UTC