nightly#44 adaptations for nightly-2025-08-25

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-08-25 nightly#44 Please review this PR. At the next toolchain release this diff will land in 'master'.

[Robin Arnez]

This is not necessary, is it?

[Kim Morrison]

No, it's not. It was a stray fix from before I undestood the issue, which apparently I failed to revert on nightly-testing. :-(

[Kim Morrison]

Hmm. It is correct on nightly-testing, not sure how the git history resulted in this being included... Let's keep an eye of for it in the next PR.