coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2018-04-20	move etc/ files to the root and remove obsolete ones	Enrico Tassi

2017-10-23	Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)	Cyril Cohen

2017-09-07	extended changelog in preparation for the next release	Cyril Cohen

2016-08-25	Enriched numClosedFieldType so that it factors a lot of theory from both ↵	Cyril Cohen
	complex and algC. The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory have been moved to the numClosedFieldType structure in ssrnum. This covers boths the uses in algC and complex.v. To that end the numClosedFieldType structure has been enriched with conjugation and 'i. Note that 'i can be deduced from the property of algebraic closure and is only here to let the user chose which definitional equality should hold on 'i. Same thing for conjC that could be written `\|x\|^+2/x, the only nontrivial (up to my knowledge) property is the fact that conjugation is a ring morphism.
2015-12-09	Moved comments on the incompatibility to INSTALL.	Assia Mahboubi
	Plus added a reference to the issue and the suggested solution in the other doc files.
2015-11-10	Adding sections for definitions in change log	amahboubi

2015-11-10	Update ChangeLog	amahboubi

2015-11-09	ChangeLog: yake Yves' suggestion into account	Enrico

2015-11-05	Changelog file created	Enrico Tassi