-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
refactor(deprecated/*): delete deprecated files #13353
Conversation
Thanks for decoupling mathlib from these files! I see that this PR is still doing some cleaning up, besides removing these files. On the topic of removing |
Hmm, this PR shouldn't be doing anything except deleting. Let me merge master again and see if it looks cleaner. |
Okay, I've added one more dependency, which cleans up some docs, and then this PR only deletes stuff. However, per the suggestion about |
I created a tracking issue at #13506. I have no intention of doing this. :-) |
If we'd prefer to leave these in place for old times sake, that's fine with me; this PR marks the milestone that they are no longer imported by the rest of mathlib!