Skip to content

Conversation

@mhuisi
Copy link
Contributor

@mhuisi mhuisi commented Oct 15, 2025

This PR fixes a bug in the unknown identifier code actions where the identifiers wouldn't be correctly minimized in nested namespaces. It also fixes a bug where identifiers would sometimes be minimized to [anonymous].

The first bug was introduced in #10619.

@mhuisi mhuisi changed the title fix: unknown identifier identifier minimization fix: unknown identifier minimization Oct 15, 2025
@mhuisi mhuisi added the changelog-server Language server, widgets, and IDE extensions label Oct 15, 2025
@mhuisi mhuisi enabled auto-merge October 15, 2025 19:21
@mhuisi mhuisi added this pull request to the merge queue Oct 15, 2025
Merged via the queue into leanprover:master with commit 4329eae Oct 15, 2025
20 of 23 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-server Language server, widgets, and IDE extensions

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant