Jason Gross (Sep 26 2022 at 15:44): Jason Gross (Sep 26 2022 at 15:44):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)
Gaëtan Gilbert (Sep 26 2022 at 15:49):what does definable mean?
Jason Gross (Sep 26 2022 at 15:54):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
Jason Gross (Sep 26 2022 at 15:54):See, e.g., https://github.com/coq/coq/issues/16540#issuecomment-1258255868
Gaëtan Gilbert (Sep 26 2022 at 16:05):you can have postponed constraints
see eg https://github.com/coq/coq/pull/13371
Jason Gross (Sep 26 2022 at 16:12):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: Apr 19 2024 at 08:01 UTC