How strong of an invariant is it that all evars definable by unification have been defined? (I'm getting lots of anomalies in tactics like `eval pattern`

and `exact`

)

what does definable mean?

All (or most) constraints of the form `?ev == <term not containing ?ev>`

have been resolved. Especially, things like `f : ?e1, x : ?e2 |- f x`

gives that `?e1`

should be resolved to `forall x : ?e2, ?e3`

, and when it's not, there seem to be lots of anomalies that crop up

See, e.g., https://github.com/coq/coq/issues/16540#issuecomment-1258255868

you can have postponed constraints

see eg https://github.com/coq/coq/pull/13371

So should all tactics be robust in the face of arbitrary postponed constraints, and I should expect the constraints that need not be postponed to be recovered and applied as needed? Or is this region of the tactic engine explicitly not supported?

Last updated: Jun 08 2023 at 04:01 UTC