Commit 2024-07-24 15:28 894061ce
View on Github →chore: fix some non-flexible simps (#15101) Found by the "flexible tactics" linter in #11821: all simp`s changed are non-terminal in the sense of the linter. Yet, all of the fixes seem like neutral or improvements to me.