coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2019-04-03	rename test-suite -> test_suite to make coq happy	Enrico Tassi

2019-04-02	identifying missing joins	Cyril Cohen

2019-02-05	we silence warnings that just pollute our logs (#275)	Enrico
	Namely: -projection-no-head-constant -redundant-canonical-projection -notation-overridden
2018-10-26	moving countalg and closed_field around	Cyril Cohen
	- countalg goes to the algebra package - finalg now get the expected inheritance from countalg - closed_field now contains the construction of algebraic closure for countable fields (previously in countalg) - proof of quantifier elimination for closed field rewritten in a monadic style
2018-04-20	Merge remote-tracking branch 'origin/pr/189'	Enrico Tassi

2018-04-20	Merge remote-tracking branch 'origin/pr/192'	Enrico Tassi

2018-04-18	Moving real_closed to another repo	Cyril Cohen

2018-04-17	move odd_order to its own repository	Enrico Tassi

2018-04-12	remove ssrtest: it now belongs to Coq	Enrico Tassi

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
2018-02-06	add 3 tests to Make	Enrico Tassi

2017-06-07	For trunk, use merged ssr plugin.	Maxime Dénès

2016-12-07	new test for "rewrite /x" when x is Opaque	Enrico Tassi

2016-12-06	add test for unfolding primitive projections	Enrico Tassi

2016-06-17	this test is now in Coq, removing it.	Enrico Tassi

2016-06-16	Port build system to trunk (ssrmatching merged in Coq)	Enrico Tassi

2016-02-25	ssrpattern: compose nicely with Tactic Notation	Enrico Tassi

2015-12-04	Move finfield to field module	Georges Gonthier

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

2015-07-17	Updating files + reorganizing everything	Cyril Cohen