coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Expand)	Author
2020-11-19	Removing duplicate clears and turning the warning into an error	Cyril Cohen
2020-04-08	fix typos in documentation: text	Antonio Nikishaev
2019-07-05	feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmas	Cyril Cohen
2019-04-29	Generalise use of `{pred T}` from coq/coq#9995	Georges Gonthier
2019-04-26	Cleaning Require and Require Imports	Cyril Cohen
2019-04-01	locking definitions to address `integral.v` divergence	Georges Gonthier
2019-04-01	Compatibility fix for Coq issue coq/#9663	Georges Gonthier
2019-04-01	Expand sample use as container in Inductive	Georges Gonthier
2019-04-01	Making {fun ...} structural and extending it to dependent functions	Georges Gonthier
2019-03-29	Merge pull request #292 from erikmd/under-support	Cyril Cohen
2019-03-21	adding ffun0	Cyril Cohen
2019-03-20	Add extra eta lemmas for the under tactic	Erik Martin-Dorel
2018-12-13	Adjust implicits of cancellation lemmas	Georges Gonthier
2018-11-21	Merge Arguments and Prenex Implicits	Anton Trunov
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-12-04	Remove redundant structures for finite powers	Georges Gonthier
2015-11-05	merge basic/ into ssreflect/	Enrico Tassi