mathlib3
refactor(*): rename metric_space_subtype to subtype.metric_space
#817

Merged

refactor(*): rename metric_space_subtype to subtype.metric_space #817

johoelzl merged 1 commit into master from subtype-metric-space

refactor(*): rename metric_space_subtype to subtype.metric_space

d610a3e3

cipher1024 assigned

avigad 7 years ago

cipher1024 requested a review from

sgouezel 7 years ago

johoelzl merged 2bf44d31 into master 7 years ago

johoelzl deleted the subtype-metric-space branch 7 years ago

Reviewers

sgouezel

Assignees

avigad

Labels

None yet

Milestone

No milestone