Commit 2026-07-15 11:24 86a97b0d

View on Github →

chore: remove all unneeded classical (#41532) This PR removes (hopefully) all occurences of classical where it is not needed. 481 out of 3132, about ~15% (much more than I had expected) Excludes MathlibTest.

Estimated changes