tactic combinator to require that a tactic changes the goal?

Stream: mathlib4

[Scott Morrison]

Some tactics (annoyingly!) don't fail if they don't make any changes. I recall at some point there being a combinator that checked that an enclosed tactic block did something, and failed otherwise. Can anyone point me to this?

[Scott Morrison]

fail_if_no_progress (the shame of having to ask motivated me to look harder, sorry :-)

[Thomas Murrills]

Just in case it’s relevant, if you need config options, I hope to put a WIP PR which adds a bunch of them out for review soon…feel free to make feature requests :)