coq-mathcomp/etc/ChangeLog, branch master Library of mathematical components formalized in Coq move etc/ files to the root and remove obsolete ones 2018-04-20T09:08:59+00:00 Enrico Tassi 2018-04-20T09:08:59+00:00 b78523ff2c3349e98686871891028069edfa7523 






Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)
2017-10-23T13:54:07+00:00

Cyril Cohen

2017-10-23T13:52:09+00:00

dd730ed0569d57944435b6bb599bffd8c382c126












extended changelog in preparation for the next release
2017-09-07T15:08:19+00:00

Cyril Cohen

2017-09-07T15:08:19+00:00

1597073304060566a2949ccd9e9ea49ab2deca9c












Enriched numClosedFieldType so that it factors a lot of theory from both complex and algC.
2016-08-24T23:39:43+00:00

Cyril Cohen

2016-08-24T23:38:44+00:00

2d824f394e8c3148e95b3374fb9903f6032ba3e6

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.





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.







Moved comments on the incompatibility to INSTALL.
2015-12-09T22:48:42+00:00

Assia Mahboubi

2015-12-09T22:48:42+00:00

2291fa456b0d385f3f8da1316d86f3b84d0aaf2d

Plus added a reference to the issue and the suggested solution in the other
doc files.





Plus added a reference to the issue and the suggested solution in the other
doc files.







Adding sections for definitions in change log
2015-11-10T10:37:36+00:00

amahboubi

2015-11-10T10:37:36+00:00

c5fd9787347cf48eb6599bad3dfff5d277f9aae2












Update ChangeLog
2015-11-10T10:16:31+00:00

amahboubi

2015-11-10T10:16:31+00:00

490d8fa0e30822caa8ea942e276ac0ed449aae1d












ChangeLog: yake Yves' suggestion into account
2015-11-09T08:55:08+00:00

Enrico

2015-11-09T08:55:08+00:00

ec504e283669ceac858bf4cc6234cedda7c50a70












Changelog file created
2015-11-05T15:26:24+00:00

Enrico Tassi

2015-10-30T14:31:31+00:00

57b0dfbf5a6af0551f48ab440e8ac96fc60c0540