Commit 2025-06-03 17:48 2f402e01

View on Github →

chore: remove dsimp when followed by simp (#25391) Now that my simp optimizations have landed, I'm testing the hypothesis that dsimp followed by simp is slower than just simp. By the way, I can't find the [dsimp, simp] library note anywhere. Has it disappeared?

Estimated changes