Skip to content

Conversation

Rob23oba
Copy link
Contributor

@Rob23oba Rob23oba commented Oct 5, 2025

This PR changes liftCommandElabM to preserve quotContext, currNamespace and openDecls when running the CommandElabM action.

Fixes #10674

@github-actions github-actions bot added the changelog-language Language features and metaprograms label Oct 5, 2025
@Rob23oba Rob23oba marked this pull request as ready for review October 5, 2025 19:00
@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 Oct 5, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ffb6142ee7fc7b8f76fd71c5672b4aeb3f8455be --onto 0b2193c7715a55246d0596a4db548c1b5b81562a. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-05 19:51:19)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ffb6142ee7fc7b8f76fd71c5672b4aeb3f8455be --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-05 19:51:21)

@Kha
Copy link
Member

Kha commented Oct 14, 2025

As mentioned in the issue, this function will, very likely, be deprecated and removed.

@Kha Kha closed this Oct 14, 2025
@Rob23oba Rob23oba deleted the fix-lift-command-elab branch October 14, 2025 13:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

liftCommandElabM breaks namespace resolution?

4 participants