Commit 2025-10-07 11:23 2f9b4817
View on Github →chore: Rename Proj.openCoverOfIsOpenCover to Proj.affineOpenCoverOfIrrelevantLESpan (#30288)
#30072 renamed AlgebraicGeometry.Scheme.openCoverOfISupEqTop to AlgebraicGeometry.Scheme.openCoverOfIsOpenCover with deprecation, but it also moved AlgebraicGeometry.Proj.openCoverOfISupEqTop to AlgebraicGeometry.Proj.openCoverOfIsOpenCover by accident, and without deprecation.
This PR is a partial revert of that Proj renaming, but also renames it to the more sensible Proj.affineOpenCoverOfIrrelevantLESpan.
Deprecation is added for the old name Proj.openCoverOfISupEqTop, but not for the current Proj.openCoverOfIsOpenCover, because this current erroneous Proj.openCoverOfIsOpenCover has only existed for 4 days.