Skip to content

Parse 0 as Set and 1 as Set+1 in universe annotations #20914

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Parse 0 as Set and 1 as Set+1 in universe annotations #20914

wants to merge 1 commit into from

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer added this to the 9.2+rc1 milestone Jul 16, 2025
@SkySkimmer SkySkimmer requested a review from a team as a code owner July 16, 2025 12:03
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 16, 2025
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 16, 2025
@SkySkimmer SkySkimmer changed the title Parse set 0 Parse 0 as Set and 1 as Set+1 in universe annotations Jul 16, 2025
@SkySkimmer
Copy link
Contributor Author

test suite failure is #20920

@SkySkimmer SkySkimmer added the needs: independent fix The PR reveals an independent bug. label Jul 17, 2025
@SkySkimmer SkySkimmer requested a review from a team as a code owner July 17, 2025 11:14
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 17, 2025
@SkySkimmer SkySkimmer added the needs: documentation Documentation was not added or updated. label Jul 17, 2025
SkySkimmer
SkySkimmer commented Jul 17, 2025
View reviewed changes
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: independent fix The PR reveals an independent bug. labels Sep 3, 2025
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Sep 3, 2025
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 19, 2025
@SkySkimmer SkySkimmer added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. and removed needs: documentation Documentation was not added or updated. labels Sep 19, 2025
@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 19, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
None yet
Milestone
9.2+rc1
Development

Successfully merging this pull request may close these issues.
1 participant
@SkySkimmer