coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2016-02-02	Do not hide critical errors with a blind catch all (fix #19)	Enrico Tassi

2016-02-02	fix debug print	Enrico Tassi

2016-02-02	Explicit error message if rewrite fails due to TC inference (fix #21)	Enrico Tassi

2016-02-01	compilation on trunk fixed	Enrico Tassi

2016-02-01	Merge pull request #20 from ppedrot/partial-fix	Enrico
	Partially fixing ML compilation on trunk.
2016-01-31	Partially fixing ML compilation on trunk.	Pierre-Marie Pédrot

2016-01-31	half-repair compilation on trunk	Enrico Tassi

2016-01-22	generalizing odd_opp	Cyril Cohen

2016-01-21	build script is now cygwin friendly	Enrico Tassi
	symlinks are not first class citizens on windows
2016-01-21	revise installer for windows	Enrico Tassi

2016-01-12	Move bullet initialization to ssreflect.v	Robbert Krebbers

2016-01-08	fix version number in initialization message	Enrico Tassi

2016-01-06	Merge pull request #13 from strub/master	Enrico
	do not use `sed -i' in ssrcoqdep -- this is not portable
2016-01-05	do not use `sed -i' in ssrcoqdep -- this is not portable	Pierre-Yves Strub
	This prevents compilation of ssreflect on OS-X/*BSD.
2015-12-26	removing mathcomp dir when removing ssreflect	Cyril Cohen

2015-12-26	packaging ssr 1.6	Cyril Cohen

2015-12-18	Changing the address of the wiki	amahboubi

2015-12-18	Typo in the github announce	amahboubi

2015-12-15	Update ANNOUNCE-1.6.md	Enrico

2015-12-15	libgraph: uglier but faster scrolling	Enrico Tassi

2015-12-14	typo	Enrico Tassi

2015-12-14	Update ANNOUNCE-github.md	Enrico

2015-12-14	fix compilation	Enrico Tassi

2015-12-14	get rid of : and basic/ in README.md	Enrico Tassi

2015-12-13	fix	Cyril Cohen

2015-12-12	removing trailing whitespaces in opam file	Cyril Cohen

2015-12-12	changing dependency	Cyril Cohen

2015-12-12	typo	Cyril Cohen

2015-12-12	modif packager ":" -> "-"	Cyril Cohen

2015-12-12	switch ":" to "-"	Cyril Cohen

2015-12-12	fixing requires in stripped odd order	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-11	coqdoc + interactive graph browsing	Enrico Tassi
	It is still rough, but better than nothing.
2015-12-11	8.5 coqdoc does not want _ to be escaped + more .css classes	Enrico Tassi

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-10	some doc for the doc building utility	Enrico Tassi

2015-12-09	Updated the address of the website in README	Assia Mahboubi
	Plus corrected some typos.
2015-12-09	Moved comments on the incompatibility to INSTALL.	Assia Mahboubi
	Plus added a reference to the issue and the suggested solution in the other doc files.
2015-12-08	Create ANNOUNCE-github.md	Enrico
	First attempt to define the organization, please comment!
2015-12-04	update license banner in .ml files	Enrico Tassi

2015-12-04	Trying a better layout of hyperlinks on github	Assia Mahboubi

2015-12-04	Trying a better layout of the .md on github	Assia Mahboubi

2015-12-04	Minor edition of the Announce.	Assia Mahboubi
	Added a few more details in the description of the components and corrected some typos.
2015-12-04	Update ANNOUNCE-1.6.md	Enrico

2015-12-04	Merge branch 'master' of https://github.com/math-comp/math-comp	Georges Gonthier

2015-12-04	Trailing whitespace removal	Georges Gonthier

2015-12-04	Ignore emacs checkpoints	Georges Gonthier

2015-12-04	Remove spurious injections	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