Skip to content

fix: lake: namespace in Lake.Util.Opaque (reapplied)#13526

Merged
tydeu merged 1 commit into
leanprover:masterfrom
tydeu:lake/opaque-namespace
Apr 24, 2026
Merged

fix: lake: namespace in Lake.Util.Opaque (reapplied)#13526
tydeu merged 1 commit into
leanprover:masterfrom
tydeu:lake/opaque-namespace

Conversation

@tydeu
Copy link
Copy Markdown
Member

@tydeu tydeu commented Apr 24, 2026

This PR reapplies #13516 which was reverted by #13517 due to a failure of GitHub's merge queue.

@tydeu tydeu added the changelog-no Do not include this PR in the release changelog label Apr 24, 2026
@tydeu tydeu changed the title fix: lake: namespace in Lake.Util.Opaque fix: lake: namespace in Lake.Util.Opaque (reapplied) Apr 24, 2026
@tydeu tydeu enabled auto-merge April 24, 2026 22:13
@tydeu tydeu added this pull request to the merge queue Apr 24, 2026
Merged via the queue into leanprover:master with commit 09fabf3 Apr 24, 2026
55 checks passed
@tydeu tydeu deleted the lake/opaque-namespace branch April 25, 2026 04:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant