-
Notifications
You must be signed in to change notification settings - Fork 314
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
chore (Topology): some universe tweaks #7638
Conversation
6c305e8
to
16439c8
Compare
e2ff401
to
5a0396d
Compare
5a0396d
to
03523ec
Compare
Reverted one last round of not-useful changes, squashed and rebased. I am sorry for all the churn. |
I don't think it is useful to give nice names to universes. Quite the opposite in fact: having |
I see. I've heard two contradictory comments now, it's hard to adhere to both... I don't care about this strongly enough to pursue this further. If you do, feel free to re-use any of this work. |
Mostly giving universes explicit/nicer names.
In two files (
ExtremallyDisconnected
andProperMap
), remove autoImplicit true.(My understanding is that this is desired; happy to revert otherwise.)