Skip to content
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

coqchk: check const_relevance #18630

Merged
merged 1 commit into from Feb 7, 2024
Merged

coqchk: check const_relevance #18630

merged 1 commit into from Feb 7, 2024

Conversation

SkySkimmer
Copy link
Contributor

Fix #18625

@SkySkimmer SkySkimmer added kind: fix This fixes a bug or incorrect documentation. part: checker The coqchk binary for validating .vo files. kind: inconsistency Proof of False accepted by the kernel and/or checker. labels Feb 6, 2024
@SkySkimmer SkySkimmer added this to the 8.19.1 milestone Feb 6, 2024
@SkySkimmer SkySkimmer requested a review from a team as a code owner February 6, 2024 11:27
@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 Feb 6, 2024
@ppedrot ppedrot self-assigned this Feb 6, 2024
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 6, 2024
@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 Feb 6, 2024
@SkySkimmer SkySkimmer requested a review from a team as a code owner February 6, 2024 12:09
@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 Feb 6, 2024
@ppedrot
Copy link
Member

ppedrot commented Feb 7, 2024

@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 Feb 7, 2024
@ppedrot
Copy link
Member

ppedrot commented Feb 7, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 3d86c1d into coq:master Feb 7, 2024
12 of 15 checks passed
@coqbot-app coqbot-app bot added this to Request 8.19.1 inclusion in Coq 8.19 Feb 7, 2024
@SkySkimmer SkySkimmer deleted the check-const-relevance branch February 8, 2024 11:42
SkySkimmer added a commit to SkySkimmer/coq that referenced this pull request Feb 19, 2024
@SkySkimmer
Backport PR coq#18630: coqchk: check const_relevance
8af0cf4
@coqbot-app coqbot-app bot moved this from Request 8.19.1 inclusion to Shipped in 8.19.1 in Coq 8.19 Feb 19, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation. kind: inconsistency Proof of False accepted by the kernel and/or checker. part: checker The coqchk binary for validating .vo files.
Projects
Coq 8.19
Shipped in 8.19.1
Milestone
8.19.1
Development

Successfully merging this pull request may close these issues.

coqchk doesn't check const_relevance
2 participants
@SkySkimmer @ppedrot