| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-25 | Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entries | Kazuhiko Sakaguchi | |
| Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com> | |||
| 2020-11-25 | Generalize `allrel` to take two lists as arguments | Kazuhiko Sakaguchi | |
| 2020-11-19 | add declare scopes | Reynald Affeldt | |
| 2020-10-29 | Switch from long suffixes to short suffixes | Kazuhiko Sakaguchi | |
| 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 | |
| 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-12-04 | Document parameter names whenever possible | Anton Trunov | |
| As suggested by @ggonthier [here](https://github.com/math-comp/math-comp/pull/249#pullrequestreview-177938295) > One of the design ideas for the `Arguments` command was that it would allow to centralise the documentation of the application of constants. In that spirit it would be in my opinion better to make as much use of this as possible, and to document the parameter names whenever possible, especially that of implicit parameters. and [here](https://github.com/math-comp/math-comp/pull/253#discussion_r237434163): > As a general rule, defined functional constants should have maximal prenex implicit arguments, as this facilitates their use as arguments to functionals, because this mimics the way function constants are treated in functional programming languages with Hindley-Milner type inference. Conversely, lemmas and theorems should have on-demand implicit arguments, possibly interspersed with explicit ones, as it's fairly common for other lemmas to have universally quantified premises; also, this makes it easier to specify such arguments with the apply: tactic. This policy may be amended for lemmas that are used as functional arguments, such as reflection or cancellation lemmas. Unfortunately there is currently no easy way to tell Coq to use different defaults for definitions and lemmas, so MathComp sticks to the on-demand default, as there are significantly more lemmas than definition, and use the Prenex Implicits to redress matters in bulk for definitions. However, this is not completely systematic, and is sometimes omitted for constants that are not used as functional arguments in the library, or inside the sections in which the definition occur, since such commands need to be repeated after the section is closed. Since Arguments commands should document the intended constant usage as best as possible, they should follow the implicits policy - even in cases such as this where the Prenex Implicits had been skipped. | |||
| 2018-11-21 | Merge Arguments and Prenex Implicits | Anton Trunov | |
| See the discussion here: https://github.com/math-comp/math-comp/pull/242#discussion_r233778114 | |||
| 2018-03-04 | Change deprecated Arguments Scope to Arguments | Jasper Hugunin | |
| 2018-02-21 | Change Implicit Arguments to Arguments in field | 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. | |||
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2015-12-04 | Add instances & lemmas for regular algebras | Georges Gonthier | |
| 2015-07-28 | update copyright banner | Enrico Tassi | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-04-09 | field for v8.5 | Cyril Cohen | |
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |