over): rename default to basic
#19217

Closed

[Merged by Bors] - chore(category_theory/limits/construction/over): rename default to basic #19217

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

chore(category_theory/limits/construction/over) rename default to basic

3a1c2726

kim-em added awaiting-review

kim-em added awaiting-CI

kim-em requested a review 3 years ago

github-actions removed awaiting-CI

jcommelin changed the title ~~chore(category_theory/limits/construction/over) rename default to basic~~ chore(category_theory/limits/construction/over): rename default to basic 3 years ago

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~chore(category_theory/limits/construction/over): rename default to basic~~ [Merged by Bors] - chore(category_theory/limits/construction/over): rename default to basic 3 years ago

bors closed this 3 years ago

bors deleted the over_default branch 3 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone

mathlib3 [Merged by Bors] - chore(category_theory/limits/construction/over): rename default to basic #19217 Closed

[Merged by Bors] - chore(category_theory/limits/construction/over): rename default to basic #19217

mathlib3
[Merged by Bors] - chore(category_theory/limits/construction/over): rename default to basic
#19217

Closed