Skip to content

refactor: cleanups after #12538#12643

Merged
datokrat merged 1 commit intomasterfrom
paul/cleanup
Feb 23, 2026
Merged

refactor: cleanups after #12538#12643
datokrat merged 1 commit intomasterfrom
paul/cleanup

Conversation

@datokrat
Copy link
Copy Markdown
Contributor

This PR removes some spurious comments after #12538.

@datokrat datokrat marked this pull request as ready for review February 23, 2026 10:22
@datokrat datokrat added this pull request to the merge queue Feb 23, 2026
@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 Feb 23, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7b3d778ab047a176130d38931794714f997a1f7b --onto 2e7fe7e79d151ee91039f086b8036252cdf9b725. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 10:29:36)

@leanprover-bot
Copy link
Copy Markdown
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 7b3d778ab047a176130d38931794714f997a1f7b --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-23 10:29:38)

Merged via the queue into master with commit 8ed6b30 Feb 23, 2026
18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

2 participants