coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
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-10-23	Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)	Cyril Cohen

2017-10-23	Merge pull request #145 from CohenCyril/new-packager	Cyril Cohen
	New packager
2017-10-19	fixed homepage	Cyril Cohen

2017-10-10	fix building with make flags	Ralf Jung
	Fixes #139
2016-11-07	update copyright banner	Assia Mahboubi

2016-09-20	[field] Remove unnecessary `Program Definition`	Emilio Jesus Gallego Arias
	Simple `Definition` should work fine here. This avoids the problem: `Error: Library Coq.Program.Tactics has to be required first.` in math-comp versions that depends on a minimal (or no) Coq stdlib. Tested on 8.5/8.6
2016-08-25	Enriched numClosedFieldType so that it factors a lot of theory from both ↵	Cyril Cohen
	complex and algC. The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory have been moved to the numClosedFieldType structure in ssrnum. This covers boths the uses in algC and complex.v. To that end the numClosedFieldType structure has been enriched with conjugation and 'i. Note that 'i can be deduced from the property of algebraic closure and is only here to let the user chose which definitional equality should hold on 'i. Same thing for conjC that could be written `\|x\|^+2/x, the only nontrivial (up to my knowledge) property is the fact that conjugation is a ring morphism.
2015-12-12	switch ":" to "-"	Cyril Cohen

2015-12-12	Revert "HACK: work around regression in 8.5"	Enrico Tassi
	This reverts commit 006565bdb5b473afff5f834e4b20320bb0a419fd. since Coq commit c6b75e1b693ab8c7af2efd1b93f04eab248e584c make this unnecessary
2015-12-10	HACK: work around regression in 8.5	Enrico Tassi
	This shall be reverted, it is there only to make ssr compile on jenkins and help the release of Coq
2015-12-04	Trailing whitespace removal	Georges Gonthier

2015-12-04	Explicit construction of finite fields	Georges Gonthier
	Two lemmas provide splitting field for a given polynomials, and a finite field of a given (prime power) order, respectively. Internal comments document type-checking performance issues that arose.
2015-12-04	Some proof refactoring	Georges Gonthier

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

2015-12-04	Remove spurious injections	Georges Gonthier

2015-12-04	Add instances & lemmas for regular algebras	Georges Gonthier

2015-12-04	Document limitation of fieldExtType cloning	Georges Gonthier
	Default cloning requires a manifest field class.
2015-12-04	Correct improper CS declaration	Georges Gonthier
	Type cast on head constant spoils projection registration (Coq misfeature).
2015-11-30	Typos in comments.	Assia Mahboubi

2015-11-20	Tested the Qed of the alternate Xirredp_FAdjoin in Coq 8.4.	Assia Mahboubi
	It's no more crashing but it's still way to long...
2015-11-10	fix INSTALL symlinks	Enrico Tassi

2015-07-28	update copyright banner	Enrico Tassi

2015-07-22	remove duplicate fields	Cyril Cohen

2015-07-22	make the opam package meta data	Cyril Cohen

2015-07-21	update opam meta-data	Cyril Cohen

2015-07-18	update to preserve backward compatibility with v8.4	Cyril Cohen

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

2015-04-09	field for v8.5	Cyril Cohen

2015-04-09	Using the From X Require Y for v8.4	Cyril Cohen

2015-04-08	makefiles that are version dependent	Cyril Cohen

2015-03-24	change finfield from field to character	Cyril Cohen

2015-03-24	metadata for solvable and field	Cyril Cohen

2015-03-09	Initial commit	Enrico Tassi