coq - The formal proof system

Age	Commit message (Collapse)	Author
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-09	Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements	letouzey
	Mostly results about Zgcd (commutativity, associativity, ...). Slight improvement of ZMicromega. Beware: some lemmas of Zdiv/ Znumtheory were asking for too strict or useless hypothesis. Some minor glitches may occur. By the way, some iff lemmas about negb in Bool.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01	Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in	letouzey
	a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t))) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28	Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are	letouzey
	now dumb wrappers around Zsqrt_plain. Wanted (dead or alive): better implemntations _and_ their proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11013 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28	CyclicAxioms: after discussion with Laurent, znz_WW and variants are	letouzey
	transformed into generic functions, and aren't anymore fields of records znz_op/znz_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11012 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-17	ZModulo: Z viewed modulo 2^digits implements CyclicAxioms	letouzey
	This isn't useful for BigN et BigZ, but it can't hurt; and moreover it's a simple way to understand CyclicAxioms. Next step: proving that Int31 is also an implementation of CyclicAxiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10942 85f007b7-540e-0410-9357-904b9bb8a0f7