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
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: Feb 05 2023 at 20:03 UTC