mathlib
cd343474 - chore(*): remove uses of `universe variable` (#9794)

Commit
4 years ago
chore(*): remove uses of `universe variable` (#9794) Most of these uses are relics of when the distinction between `universe` and `universe variable` was more significant. There is still a difference inside sections, but it's an edge case and I don't think any of these uses are consciously trying to handle the edge case.
Author
Parents
Loading