coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2019-12-11	Fixes in naming, mixins, doc and canonical ordering	Cyril Cohen
	- comparer -> compare (in order.v) - eq constructor of compare goes last - "x < y" is matched before "x > y" - "x <= y" is matched before "x >= y" - adding prod and lexi ordering on tuple - adding missing CS - edit CHANGELOG
2019-04-29	Generalise use of `{pred T}` from coq/coq#9995	Georges Gonthier
	Use `{pred T}` systematically for generic _collective_ boolean predicate. Use `PredType` to construct `predType` instances. Instrument core `ssreflect` files to replicate these and other new features introduces by coq/coq#9555 (`nonPropType` interface, `simpl_rel` that simplifies with `inE`).
2019-04-26	Cleaning Require and Require Imports	Cyril Cohen

2019-03-20	Add extra eta lemmas for the under tactic	Erik Martin-Dorel
	Related: coq/coq#9651
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-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-11-15	Tweak code related to canonical mixins	Anton Trunov
	Remove some unused canonical mixins. Change simplification behavior of concrete comparison functions to allow for better simplification using unfolding and sebsequent folding back e.g. with `rewrite !eqE /= -!eqE`. A bit of cleanup for `Prenex Implicits` declarations. Document some explanations by G. Gonthier.
2018-07-12	Replace all the CoInductives with Variants	Kazuhiko Sakaguchi

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

2016-11-07	update copyright banner	Assia Mahboubi

2015-11-05	merge basic/ into ssreflect/	Enrico Tassi