| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-20 | fix symlinks to README, INSTALL and LICENSE | Enrico Tassi | |
| 2018-03-04 | Change deprecated Arguments Scope to Arguments | Jasper Hugunin | |
| 2018-02-21 | Change Implicit Arguments to Arguments in fingroup | Jasper Hugunin | |
| 2018-02-06 | running semi-automated linting on the whole library | 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-08-13 | Fix typo in fingroup documentation | Patrick Massot | |
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 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-12 | switch ":" to "-" | Cyril Cohen | |
| 2015-11-10 | fix INSTALL symlinks | Enrico Tassi | |
| 2015-11-06 | basic has disappeared | Cyril Cohen | |
| 2015-07-28 | update copyright banner | Enrico Tassi | |
| 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 |