| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-10-07 | Turn class_of records into primitive records and get rid of the xclass idiom | Kazuhiko Sakaguchi | |
| 2019-04-26 | Cleaning Require and Require Imports | Cyril Cohen | |
| 2019-04-02 | Fix inheritances in countalg and finalg (the 2nd attempt) | Kazuhiko Sakaguchi | |
| 2018-12-04 | Remove `_ : Type` from packed classes | Anton Trunov | |
| This increases performance 10% - 15% for Coq v8.6.1 - v8.9.dev. Tested on a Debain-based 16-core build server and a Macbook Pro laptop with 2,3 GHz Intel Core i5. | | Compilation time, old | Compilation | Speedup | | | (mathcomp commit 967088a6f87) | time, new | | | Coq 8.6.1 | 10min 33s | 9min 10s | 15% | | Coq 8.7.2 | 10min 12s | 8min 50s | 15% | | Coq 8.8.2 | 9min 39s | 8min 32s | 13% | | Coq 8.9.dev(05d827c800544) | 9min 12s | 8min 16s | 11% | | | | | | It seems Coq at some point fixed the problem `_ : Type` was supposed to solve. | |||
| 2018-10-26 | moving countalg and closed_field around | Cyril Cohen | |
| - countalg goes to the algebra package - finalg now get the expected inheritance from countalg - closed_field now contains the construction of algebraic closure for countable fields (previously in countalg) - proof of quantifier elimination for closed field rewritten in a monadic style | |||
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |