mathlib3
[Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153
#19230

Closed

[Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153 #19230

kim-em wants to merge 1 commit into master from revert_19153

Revert "chore(topology/sheaves/*): universe generalizations (#19153)"

49f736a7

kim-em added awaiting-review

kim-em added awaiting-CI

kim-em requested a review 2 years ago

github-actions added modifies-synchronized-file

github-actions added delegated

github-actions removed awaiting-review

github-actions removed awaiting-CI

github-actions added ready-to-merge

bors changed the title ~~chore(topology/sheaves): revert universe generalizations from #19153~~ [Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153 2 years ago

bors closed this 2 years ago

bors deleted the revert_19153 branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge delegated modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153 #19230 Closed

[Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153 #19230

mathlib3
[Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153
#19230

Closed