mathlib3
chore(data/polynomial): clean up commented code
#1251

Merged

chore(data/polynomial): clean up commented code #1251

ChrisHughes24 merged 1 commit into master from jcommelin-patch-1

chore(data/polynomial): clean up commented code

e0dcf12c

jcommelin requested a review 6 years ago

ChrisHughes24 added ready-to-merge

ChrisHughes24 approved these changes on 2019-07-22

ChrisHughes24 merged b5a641e8 into master 6 years ago

ChrisHughes24 deleted the jcommelin-patch-1 branch 6 years ago

Reviewers

ChrisHughes24

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone