| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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-08-06 | changing companionmx to a more standard one | Cyril Cohen | |
| 2018-08-03 | update ChangeLog and doc | Cyril Cohen | |
| 2018-08-01 | Companion matrix of a polynomial | Cyril Cohen | |
| 2018-02-21 | Change Implicit Arguments to Arguments in algebra | 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-07-28 | update copyright banner | Enrico Tassi | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-04-09 | Using the From X Require Y for v8.4 | Cyril Cohen | |
| 2015-04-08 | packaging for v8.5 | Cyril Cohen | |
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |