Commit 2026-07-07 15:21 d8d7c660

View on Github →

chore: prefer open scoped Classical over open Classical (#41414) As suggested here. Replace open Classical with open scoped Classical whenever possible (only like open Classical 5 remain), excluding MathlibTest. 6 more open Classical were found to be entirely redundant. The next PR in this series will try to remove redundant open scoped Classical. (I would also do classical but my computer is a bit too slow for that...)

Estimated changes