| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-19 | add declare scopes | Reynald Affeldt | |
| 2020-06-09 | fix coq 8.12 warnings | Cyril Cohen | |
| 2020-05-16 | A few more revisions | Kazuhiko Sakaguchi | |
| 2020-04-08 | fix typos in documentation: text | Antonio Nikishaev | |
| 2019-04-26 | Cleaning Require and Require Imports | Cyril Cohen | |
| 2018-12-13 | Adjust implicits of cancellation lemmas | Georges Gonthier | |
| Like injectivity lemmas, instances of cancellation lemmas (whose conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or `ocancel`) are passed to generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should not have trailing on-demand implicits _just before_ the `cancel` conclusion, as these would be inconvenient to insert (requiring essentially an explicit eta-expansion). We therefore use `Arguments` or `Prenex Implicits` directives to make all such arguments maximally inserted implicits. We don’t, however make other arguments implicit, so as not to spoil direct instantiation of the lemmas (in, e.g., `rewrite -[y](invmK injf)`). We have also tried to do this with lemmas whose statement matches a `cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern unification will pick up `f = fun x => E[x]`). We also adjusted implicits of a few stray injectivity lemmas, and defined constants. We provide a shorthand for reindexing a bigop with a permutation. Finally we used the new implicit signatures to simplify proofs that use injectivity or cancellation lemmas. | |||
| 2018-12-11 | Fix some new warnings emitted by Coq 8.10: | Anton Trunov | |
| ``` Warning: Adding and removing hints in the core database implicitly is deprecated. Please specify a hint database. [implicit-core-hint-db,deprecated] ``` | |||
| 2018-12-04 | Remove pack constructors | Anton Trunov | |
| 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-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-07-12 | Replace all the CoInductives with Variants | Kazuhiko Sakaguchi | |
| 2018-02-21 | Change Implicit Arguments to Arguments in ssreflect | Jasper Hugunin | |
| 2018-02-06 | running semi-automated linting on the whole library | Cyril Cohen | |
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2015-11-05 | merge basic/ into ssreflect/ | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |