coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Updating headers.	herbelin	2012-08-08
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def	letouzey	2011-06-28
*	Numbers: change definition of divide (compat with Znumtheory)	letouzey	2011-06-24
*	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey	2011-06-20
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	Zdiv: results about eqm (the equality modulo some N) under a section	letouzey	2011-05-05
*	ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2	letouzey	2010-12-09
*	Numbers and bitwise functions.	letouzey	2010-12-06
*	Integer division: quot and rem (trunc convention) in addition to div and mod	letouzey	2010-11-10
*	Add small utility lemmas about nat/P/Z/Q arithmetic.	letouzey	2010-11-02
*	Numbers: new functions pow, even, odd + many reorganisations	letouzey	2010-10-14
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Numbers: properties of min/max with respect to 0,S,P,add,sub,mul	letouzey	2010-02-09
*	ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType	letouzey	2010-02-09
*	Support "Local Obligation Tactic" (now the default in sections).	msozeau	2010-01-11
*	Numbers abstract layer: more Module Type, used especially for divisions.	letouzey	2010-01-05
*	Zdiv seen as a quasi-instantation of generic ZDivFloor from theories/Numbers	letouzey	2010-01-05
*	Remove various useless {struct} annotations	letouzey	2009-11-02
*	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey	2009-09-28
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements	letouzey	2009-09-09
*	Zdiv: eqm (equality modulo some N) can now be declared as Parametric Relation	letouzey	2008-10-20
*	Cyclic31: migrate auxiliary lemmas to their legitimate files	letouzey	2008-05-27
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	one forgotten compatibility lemma	letouzey	2008-02-08
*	Adding Zdiv_le_compat_l	thery	2008-01-22
*	A result about Zsgn(a/b), both for Zdiv and ZOdiv	letouzey	2007-11-10
*	First reasonably complete version of ZOdiv, including some properties	letouzey	2007-11-10
*	setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.	letouzey	2007-11-08
*	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey	2007-11-06
*	Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...	letouzey	2007-11-06
*	Adding Qround.v (and helper lemmas and hints)	roconnor	2007-11-01
*	Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le	roconnor	2007-10-19
*	normalisation (by closure) was not performed under fixpoints	barras	2007-07-12
*	Mise en forme des theories	notin	2006-10-17
*	commit de field + renommages	barras	2006-09-26
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Nouvelle en-tête	herbelin	2004-07-16
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Require	herbelin	2003-11-13
*	qq petit ajouts à Zdiv	letouzey	2003-11-13
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-21
*	Zdiv plus efficace: r+r -> 2*r	letouzey	2003-09-05
*	Ajout Open Scope	herbelin	2003-04-09