Skip to content

Conversation

@leanprover-community-bot-assistant
Copy link
Collaborator

I am happy to remove some deprecated declarations for you!

@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 25, 2025
@adomani adomani closed this Sep 25, 2025
@adomani adomani deleted the deprecated-decls branch September 25, 2025 18:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants