Commit 2026-03-10 04:41 155346a7

View on Github →

chore: remove obsolete set_option backward.* (#36424) Removes another 45 no-longer-needed set_option backward.*, in preparation for moving Mathlib to v4.29.0-rc6.

Estimated changes