| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-12 | Adding row/col/block_mx_eq0 | Cyril Cohen | |
| 2017-11-27 | following @ggonthier remark. | Cyril Cohen | |
| 2017-11-23 | Add addrKA and subrKA (addrK and addrNK modulo Associativity) | Cyril Cohen | |
| 2017-10-30 | Fix obsolete vernacular syntax for locality. | Maxime Dénès | |
| It was emitting a deprecation warning and will soon be removed from Coq. | |||
| 2017-10-23 | Remove compatibility with Coq.8.4 (and compatibility hacks that went with it) | Cyril Cohen | |
| 2017-10-23 | Merge pull request #145 from CohenCyril/new-packager | Cyril Cohen | |
| New packager | |||
| 2017-10-19 | fixed homepage | Cyril Cohen | |
| 2017-10-10 | fix building with make flags | Ralf Jung | |
| Fixes #139 | |||
| 2017-02-04 | adding rquot_comRingType | Cyril Cohen | |
| 2016-11-17 | Merge remote-tracking branch 'upstream/master' into fixdoc | Florent Hivert | |
| 2016-11-16 | Fixes the doc of mxalgebra | Florent Hivert | |
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-10-24 | wip shorter proof dec factor theorems | Cyril Cohen | |
| 2016-08-25 | Factor theorem for decidable fields, (inspired by PY Strub) | 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. | |||
| 2016-03-15 | Merge pull request #34 from strub/master | Enrico | |
| all_algebra now exports zmodp | |||
| 2016-03-15 | all_algebra now exports zmodp | Pierre-Yves Strub | |
| 2016-02-06 | typo in int divn1 -> divz1 | thery | |
| 2015-12-12 | switch ":" to "-" | Cyril Cohen | |
| 2015-12-04 | Add finLmodType, finLalgType and finAlgType instances | Georges Gonthier | |
| 2015-12-04 | Remove more redundant power type structures | Georges Gonthier | |
| 2015-12-04 | Correct join values to baseFingroupType | Georges Gonthier | |
| These were all GRing.Zmodule.sort, instead of the corresponding sort in GRing (Ring.sort, Comin.sort, etc). | |||
| 2015-12-04 | Add missing export | Georges Gonthier | |
| 2015-11-10 | fix INSTALL symlinks | Enrico Tassi | |
| 2015-07-28 | update copyright banner | Enrico Tassi | |
| 2015-07-22 | forgotten import | Cyril Cohen | |
| 2015-07-22 | remove duplicate fields | Cyril Cohen | |
| 2015-07-22 | make the opam package meta data | Cyril Cohen | |
| 2015-07-21 | update opam meta-data | Cyril Cohen | |
| 2015-07-18 | update to preserve backward compatibility with v8.4 | Cyril Cohen | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-04-09 | Using the From X Require Y for v8.4 | Cyril Cohen | |
| 2015-04-08 | packaging for v8.5 | Cyril Cohen | |
| 2015-04-08 | makefiles that are version dependent | Cyril Cohen | |
| 2015-03-19 | packaging fingroup and algebra | Cyril Cohen | |
| The files zmodp and cyclic in fingroup had dependecies in algebra so I put them there. I'm not convinced it's the best solution to this problem. Maybe more subdivisions in algebra would bring a better solution? (Maybe we should send the whole problem to a solver? :P) | |||
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |