coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
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-04-18	Remove unused `Require`s and a hint directive from interval.v	Kazuhiko Sakaguchi

2019-02-07	Add the eqType instance for intervals, le_bound(l\|r)_anti, and ↵	Kazuhiko Sakaguchi
	itv_intersection, redefine prev_of_itv and itv_decompose using lersif, extend itv_rewrite, simplify proofs (#271)
2019-01-29	Add some theorems on lersif and intervals (#269)	Kazuhiko Sakaguchi
	* Add some theorems on lersif and intervals * Add more theorems on lersif * Remove needless parens * ChangeLog * Move lersifN * Add lersif_anti
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-02-21	Change Implicit Arguments to Arguments in algebra	Jasper Hugunin

2018-02-06	running semi-automated linting on the whole library	Cyril Cohen

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