coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
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	Add elementary abelian finite modules lemmas to abelian	Georges Gonthier
	This factors proofs in mxabelem and finfield and removes dependencies between these two files.
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-12-04	Add finLmodType, finLalgType and finAlgType instances	Georges Gonthier

2015-12-04	Removed spurious injection & clean up proof	Georges Gonthier

2015-12-04	Remove more redundant power type structures	Georges Gonthier

2015-12-04	Correct join values to baseFingroupType	Georges Gonthier
	These were all GRing.Zmodule.sort, instead of the corresponding sort in GRing (Ring.sort, Comin.sort, etc).
2015-12-04	Remove redundant structures for finite powers	Georges Gonthier

2015-12-04	Add missing export	Georges Gonthier

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-20	Typo.	Assia Mahboubi

2015-11-20	Typos	Assia Mahboubi

2015-11-10	fix INSTALL symlinks	Enrico Tassi

2015-11-10	Adding sections for definitions in change log	amahboubi

2015-11-10	Update ChangeLog	amahboubi

2015-11-09	ChangeLog: yake Yves' suggestion into account	Enrico

2015-11-06	First stab at INSTALL	Enrico Tassi

2015-11-06	basic has disappeared	Cyril Cohen

2015-11-06	Makefile to create a tar ball	Enrico Tassi

2015-11-05	Changelog file created	Enrico Tassi

2015-11-05	Update .git* conf files to ignore/exclude cruft	Enrico Tassi

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

2015-10-26	Added support for highlighting 'isn't' in PG.	Assia Mahboubi

2015-10-26	Added suport for highlighting gen(erally) have in PG.	Assia Mahboubi

2015-10-26	Small updates in the documentation of the customization of PG.	Assia Mahboubi

2015-10-26	Restaured the config files (including doc) for PG in the ssreflect package.	Assia Mahboubi

2015-09-27	fix compilation on trunk	Enrico Tassi

2015-09-24	Fix compilation on 8.5	Enrico Tassi

2015-09-01	Fix typo in README.	Maxime Dénès

2015-08-24	Compare pattern heads (constants) up to "univs"	Enrico Tassi
	So that Universe Polymorphic constants are compared "correctly", i.e. not discriminated by the pattern filtering phase (verbatim head comparison) but eventually by unification.
2015-07-30	fix trunk compilation	Enrico Tassi

2015-07-29	Update README.md	amahboubi
	A few typos and minor changes
2015-07-29	fix PF	Cyril Cohen

2015-07-29	add a missing From ...	Cyril Cohen

2015-07-29	Update README.md	Cyril Cohen
	simpler way of doing local opam pin
2015-07-29	First stab at the README (displayed on github)	Enrico Tassi

2015-07-29	fix Makefiles	Enrico Tassi

2015-07-29	fix path of Makefile.coq-makefile	Enrico Tassi

2015-07-28	update copyright banner	Enrico Tassi

2015-07-28	factor common Makefile stuff	Enrico Tassi

2015-07-22	Add a From ...	Cyril Cohen

2015-07-22	next blind fix	Cyril Cohen

2015-07-22	blind fix	Cyril Cohen

2015-07-22	blind patch by Enrico	Cyril Cohen