coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2020-09-29	rename mem_imset2 to imset2_f (with deprecation)	Christian Doczkal

2020-09-29	rename mem_imset to imset_f (with deprecation)	Christian Doczkal

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-07-12	Replace all the CoInductives with Variants	Kazuhiko Sakaguchi

2018-03-04	Change deprecated Arguments Scope to Arguments	Jasper Hugunin

2018-02-21	Change Implicit Arguments to Arguments in fingroup	Jasper Hugunin

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