| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-17 | move odd_order to its own repository | Enrico Tassi | |
| 2018-03-04 | Change deprecated Arguments Scope to Arguments | Jasper Hugunin | |
| 2018-02-22 | Change Implicit Arguments to Arguments in odd_order | Jasper Hugunin | |
| 2018-02-06 | fixing things that @ggonthier and @ybertot spotted and some I spotted | Cyril Cohen | |
| 2018-02-06 | running semi-automated linting on the whole library | Cyril Cohen | |
| 2017-11-06 | Fix the only remaining spurious injection in the entire codebase. | Maxime Dénès | |
| We may want to make it an error, now that the transition period has been long enough. | |||
| 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 | |||
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-09-16 | Refactoring of binonial | thery | |
| Variable renaming from 'C(m,n) to 'C(n,m) Renaming theorem mul_Sm_binn to mul_bin_diag Adding theorems mul_bin_left mul_bin_right | |||
| 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-02-22 | PF5: more predictable rewrite line (needed by rewrite using 8.5 refiner) | Enrico Tassi | |
| 2015-12-14 | fix compilation | Enrico Tassi | |
| 2015-12-13 | fix | Cyril Cohen | |
| 2015-12-12 | switch ":" to "-" | Cyril Cohen | |
| 2015-12-12 | fixing requires in stripped odd order | Cyril Cohen | |
| 2015-12-04 | Remove spurious injections | Georges Gonthier | |
| 2015-11-10 | fix INSTALL symlinks | Enrico Tassi | |
| 2015-07-29 | fix PF | Cyril Cohen | |
| 2015-07-29 | add a missing From ... | 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 | packaging odd_order | Cyril Cohen | |
| 2015-04-09 | Using the From X Require Y for v8.4 | Cyril Cohen | |
| 2015-04-08 | makefiles that are version dependent | Cyril Cohen | |
| 2015-03-24 | metadata for solvable and field | Cyril Cohen | |
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |