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

fix: revert creates natural metavariable goal #6145

Merged
merged 3 commits into from
Nov 21, 2024
Merged

fix: revert creates natural metavariable goal #6145

merged 3 commits into from
Nov 21, 2024

Conversation

JovanGerb
Copy link
Contributor

This PR fixes the revert tactic so that it creates a syntheticOpaque metavariable as the new goal, instead of a natural metavariable

I reported it on Zulip

@JovanGerb JovanGerb marked this pull request as draft November 21, 2024 00:34
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 21, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 21, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6145
c125485
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 21, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6145
a8aeda3
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 21, 2024 •
edited
Loading

Mathlib CI status (docs):

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 21, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 21, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6145
fa04d61
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 21, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6145
0ac7044
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 21, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6145
6800162
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 21, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6145
c68ddf3
@JovanGerb JovanGerb marked this pull request as ready for review November 21, 2024 10:14
@kmill kmill added the changelog-language Language features, tactics, and metaprograms label Nov 21, 2024
@kmill kmill added this pull request to the merge queue Nov 21, 2024
@kmill
Copy link
Collaborator

kmill commented Nov 21, 2024

Thanks!

Merged via the queue into leanprover:master with commit b7248d5 Nov 21, 2024
18 of 19 checks passed
@JovanGerb JovanGerb deleted the revertMetavarKind branch November 22, 2024 11:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@JovanGerb @leanprover-community-bot @kmill