mathlib3
chore(*): renaming files constructing category instances
#1432

Merged

chore(*): renaming files constructing category instances #1432

mergify merged 2 commits into master from category_instances_reorg2

chore(*): renaming files constructing category instances

1e567f98

kim-em requested a review 6 years ago

rwbarton approved these changes on 2019-09-11

Merge remote-tracking branch 'origin/master' into HEAD

bfd530ca

rwbarton added ready-to-merge

mergify merged e27142aa into master 6 years ago

mergify deleted the category_instances_reorg2 branch 6 years ago

Reviewers

rwbarton

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone