aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/real_closed/complex.v
AgeCommit message (Expand)Author
2018-04-18Moving real_closed to another repoCyril Cohen
2018-02-06fixing things that @ggonthier and @ybertot spotted and some I spottedCyril Cohen
2018-02-06running semi-automated linting on the whole libraryCyril Cohen
2016-11-07update copyright bannerAssia Mahboubi
2016-08-25Enriched numClosedFieldType so that it factors a lot of theory from both comp...Cyril Cohen
2015-07-28update copyright bannerEnrico Tassi
2015-07-17Updating files + reorganizing everythingCyril Cohen
2015-03-09Initial commitEnrico Tassi