| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-06 | Update README.md | Cyril Cohen | |
| fixes #175 | |||
| 2018-02-06 | add 3 tests to Make | Enrico Tassi | |
| 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 | |
| 2018-02-05 | Merge pull request #176 from gares/fix/card_inj_ffuns | Assia Mahboubi | |
| tide up proof of card_inj_ffuns | |||
| 2018-02-05 | tide up proof of card_inj_ffuns | Enrico Tassi | |
| 2018-01-26 | Merge pull request #171 from CohenCyril/mxdirect_delta | Cyril Cohen | |
| The spaces generated by some delta_mx are in a direct sum | |||
| 2017-12-20 | Merge pull request #172 from CohenCyril/row_mx_eq0 | Assia Mahboubi | |
| Adding row/col/block_mx_eq0 | |||
| 2017-12-15 | Merge pull request #170 from CohenCyril/mulr_eq1E | Cyril Cohen | |
| Using x * y = 1 and x / y = 1 to derive invertibility and the inverse | |||
| 2017-12-15 | Merge pull request #157 from ybertot/add-subset-orbit-theorems | Cyril Cohen | |
| Adds generalizations of theorems relying on injectivity | |||
| 2017-12-14 | Merge pull request #167 from hivert/PR2 | Cyril Cohen | |
| Resubmitted lemma reshape_index_leq for discussion | |||
| 2017-12-14 | Merge pull request #155 from erikmd/fix/gh-61 | Cyril Cohen | |
| Update v8.5 plugin to fix math-comp/math-comp#61 | |||
| 2017-12-14 | The spaces generated by some delta_mx are in a direct sum | Cyril Cohen | |
| proof by @ggonthier | |||
| 2017-12-14 | Merge pull request #168 from hivert/allpairs | Cyril Cohen | |
| bigop with allpairs | |||
| 2017-12-14 | Using x * y = 1 and x / y = 1 to derive the inverse | Cyril Cohen | |
| fixes #169 | |||
| 2017-12-12 | Adding row/col/block_mx_eq0 | Cyril Cohen | |
| 2017-12-12 | refactored proof and renamed to reshape_leq and removed spurious hypothesis | Cyril Cohen | |
| 2017-12-12 | bigop with allpairs | Florent Hivert | |
| 2017-12-12 | New lemma reshape_index_leq | Florent Hivert | |
| 2017-12-12 | shortening and refactoring | Cyril Cohen | |
| 2017-12-12 | Adds generalizations of theorems relying on injectivity | Yves Bertot | |
| - f_finv - finv_f - fconnect_sym - iter_order - iter_finv - cycle_orbit - fpath_finv (* I need to sub-theorems for this case. *) All generalizations are named "..._in" the existing theorems are now instances of the generalizations. | |||
| 2017-12-11 | Merge pull request #162 from CohenCyril/CONTRIBUTING | Cyril Cohen | |
| Draft contributing guide | |||
| 2017-12-11 | Merge pull request #160 from CohenCyril/subr_trans | Cyril Cohen | |
| Add addrKA and subrKA (addrK and addrNK modulo Associativity) | |||
| 2017-12-11 | Merge pull request #166 from hivert/PR | Cyril Cohen | |
| Resubmitted missing lemma in seq.v | |||
| 2017-12-11 | Missing lemmas in seq | Florent Hivert | |
| 2017-12-11 | fixing typos | Cyril Cohen | |
| 2017-11-30 | Minor updates in the readme | Assia Mahboubi | |
| 2017-11-30 | README: remove broken link to the wiki about software | Enrico | |
| 2017-11-30 | Merge pull request #165 from ejgallego/readme_pass | Enrico | |
| [doc] Attempt to tweak README based on the discussion. | |||
| 2017-11-29 | [doc] Attempt to tweak README based on the discussion. | Emilio Jesus Gallego Arias | |
| 2017-11-27 | following @ggonthier remark. | Cyril Cohen | |
| 2017-11-24 | Draft contributing guide, fixes #158 | Cyril Cohen | |
| 2017-11-23 | Add addrKA and subrKA (addrK and addrNK modulo Associativity) | Cyril Cohen | |
| 2017-11-21 | Merge pull request #115 from strub/uniqP | Cyril Cohen | |
| Reflection lemmas for `seq.uniq` | |||
| 2017-11-14 | Update v8.5 plugin to fix math-comp/math-comp#61 | Erik Martin-Dorel | |
| 2017-11-07 | Update README.md | Cyril Cohen | |
| 2017-11-07 | Opam installation instruction update | Cyril Cohen | |
| For released or dev versions | |||
| 2017-11-06 | Merge pull request #154 from maximedenes/nothing-to-inject | Enrico | |
| Fix the only remaining spurious injection in the entire codebase. | |||
| 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 | Merge pull request #153 from maximedenes/remove-obsolete-locality | Enrico | |
| Fix obsolete vernacular syntax for locality. | |||
| 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-26 | Merge pull request #149 from CohenCyril/no-compat-coq.8.4 | Cyril Cohen | |
| Remove compatibility with Coq.8.4 | |||
| 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-20 | Merge pull request #140 from RalfJung/make | Enrico | |
| fix building with make flags | |||
| 2017-10-20 | Merge pull request #143 from RalfJung/coq-version | Enrico | |
| fix Coq version detection on Windows, and in case there are warnings | |||
| 2017-10-20 | reproduce github archive locally rather than downloading, much faster | Cyril Cohen | |
| 2017-10-20 | improved package generator | Cyril Cohen | |
| 2017-10-19 | fixed homepage | Cyril Cohen | |
| 2017-10-19 | fix coq version | Cyril Cohen | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |