Michael Soegtrop has marked this topic as resolved.
Michael Soegtrop said:
So a difference between Ltac2
refineis that Ltac1
Do you think I should open an issue to adjust the behaviour of Ltac2
refine(the notation, not the
Control.refinefunction) to that of Ltac1
Yes. For ease of translation from Ltac1, I think the version that does not shelve should be named
simple refine, and the version that shelves everything should be named
eexact. If this is too ad-hoc, then instead there should be another file "Ltac1CompatNotations", or something, which (re)defines notations to more closely match with Ltac1, maybe making them all deprecated (with no scheduled removal date) to indicate that they should not be used in new scripts, only in porting.
I think most people who build elaborate automation based on Ltac2 use the functions and not the notations and few people are using Ltac2 in proof mode, so my expectation is that changing this breaks close to nothing, but one would have to see. The nice thing about changing the notations is that it is then very explicit what they do.
My thought with compat was less about whether or not the change breaks things and more about whether or not Ltac1's design here is good enough to keep in Ltac2 (e.g., maybe this difference was deliberate on @Pierre-Marie Pédrot 's part)
Last updated: Nov 29 2023 at 22:01 UTC