coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
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-12-04	fix coq-mathcomp-ssreflect opam package description	Enrico Tassi

2015-12-03	Removing the only use of globTacticIn.	Pierre-Marie Pédrot

2015-12-03	fix compilation on trunk (thanks PMP)	Enrico Tassi

2015-12-03	fix: autogen + abstract variables clash	Enrico Tassi

2015-12-03	fix: elim/v handles eliminator from Derive Inversion (issue #2)	Enrico Tassi
	Also: - fix elim trying to saturate too much and not raising the expected exn - fix fill_occ_pattern when occ is {-}, it used to lose the instantiation obtained by matching the term
2015-12-03	Add commands to trace the matching algorithm	Enrico Tassi

2015-12-03	fix: Hint View is not a Query	Enrico Tassi

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-06	basic has disappeared	Cyril Cohen

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-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	fix PF	Cyril Cohen

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

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

2015-07-22	forgotten import	Cyril Cohen

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-21	keeping track of the changes for trunk (import from svn)	Cyril Cohen

2015-07-21	fix Makefile for trunk	Cyril Cohen