Most tactics are in some sense based on refine in that they replace a unification variable with a partially defined term. What tactics, if any, cannot be accomplished this way and you have to change the proof term outside of the unification variable corresponding to the goal

Nice, thank you. This is a good example. This command instantiates unification variables and thus fleshes out an existing (partially defined) term with more structure. Are there tactics which rearrange already existing structure of the proof tree. For example, the existing proof term is t[X] where X is some unification variable, and after the tactic is executed, the proof term becomes

```
match a with (...) return (...) in
| constr s1 s2 => t[f(s1, s2, Y)]
end
```

for some unification variable Y.

My point is that we are not just (partially) instantiating unification variables but perhaps adding new structure above and around the existing proof term which changes the context in which the metavariable X lives?

My point is that we are not just (partially) instantiating unification variables but perhaps adding new structure above and around the existing proof term which changes the context in which the metavariable X lives?

I don't think that's allowed

the structure of the proof data is this stuff https://github.com/coq/coq/blob/dc2dd34bd23e55c3deeb556c5136c72ea3352e99/proofs/proof.ml#L111-L113

`entry`

is the proof term of the whole proof, typically starts as an evar

then as we run tactics they may define evars in the evar map (which is inside the Proofview.proofview)

undefining evars is not allowed (modulo some hacks in ssr which AFAIK are supposed to be local)

yes, basically the only thing you can do is define evars and create new ones (+ additional metadata storing)

Last updated: Sep 23 2023 at 07:01 UTC