coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2018-07-31	agressive fix for duplicated files!	Cyril Cohen

2018-07-12	Replace all the CoInductives with Variants	Kazuhiko Sakaguchi

2018-03-21	Declare prenex implicits for `Some_inj`	Anton Trunov
	This backports the changes from Coq's [PR #6911](https://github.com/coq/coq/pull/6911) And also fixes a typo in doc comments
2018-02-26	Add ssrmatching.v transitional file	Erik Martin-Dorel
	The content of this file is similar to that of ssrfun.v and aims to increase compatibility with Coq 8.6+ for third-party libraries that depend on both math-comp and ssrmatching.v Close #63
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.
2017-06-09	fix compilation on 8.6	Enrico Tassi

2016-12-06	Use Tacred.unfoldn [AllOccurrences..] to work around Coq #5250	Enrico Tassi

2016-12-06	rewrite /primitive_projection is now supported (fix #85)	Enrico Tassi

2016-11-08	fix compilation on 8.6 and trunk	Enrico Tassi

2016-11-07	update copyright banner	Assia Mahboubi

2016-09-27	Add a typing colon in the output of the Search ssreflect vernacular.	Erik Martin-Dorel

2016-08-25	FIX: adding missing version of the ssreflect plugin that compiles with Coq v8.6.	Matej Kosik
	The committed files represent copies of the ssreflect plugin for Coq trunk taken from commit c353aa5 which is the last commit in which ssreflect plugin marked for Coq trunk is usable with both, Coq trunk as well as Coq v8.6.