coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Pos.iter arguments in a better order for cbn.	Pierre Boutillier	2014-05-02
*	More dynamic argument scopes	letouzey	2013-07-17
*	Updating headers.	herbelin	2012-08-08
*	BinPos/BinInt/BinNat : fix some argument scopes	letouzey	2012-07-06
*	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
*	BinInt: a forgotten scope for a notation	letouzey	2012-06-19
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	BinInt: more structured scripts thanks to bullets and { }	letouzey	2011-08-09
*	Cleanup of files related with power over Z.	letouzey	2011-07-01
*	Deletion of useless Zdigits_def	letouzey	2011-06-28
*	Numbers: change definition of divide (compat with Znumtheory)	letouzey	2011-06-24
*	Some more cleanup of Zorder	letouzey	2011-06-23
*	Some migration of results from BinInt to Numbers	letouzey	2011-06-20
*	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey	2011-06-20
*	Minimal lemmas about Z.gt, N.gt and co	letouzey	2011-05-05
*	BinInt: Z.add become the alternative Z.add'	letouzey	2011-05-05
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	Modularization of BinPos + fixes in Stdlib	letouzey	2011-05-05
*	Definitions of positive, N, Z moved in Numbers/BinNums.v	letouzey	2011-05-05
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	In passing, very quick uniformization of coqdoc headers in a few files.	herbelin	2010-12-09
*	Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits	letouzey	2010-11-18
*	Add small utility lemmas about nat/P/Z/Q arithmetic.	letouzey	2010-11-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType	letouzey	2010-02-09
*	DecidableType: A specification via boolean equality as an alternative to eq_dec	letouzey	2009-11-10
*	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
*	- Modification de la déf de minus et pred conformément aux remarques de	herbelin	2008-05-28
*	Cyclic31: migrate auxiliary lemmas to their legitimate files	letouzey	2008-05-27
*	- Changement du code de Zplus pour accomoder ring qui sinon prend une	herbelin	2008-05-11
*	Proposal of a nice notation for constructors xI and xO of type positive	letouzey	2008-02-10
*	setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.	letouzey	2007-11-08
*	In agreement with Laurent Thery, start migration of auxiliary results	letouzey	2007-11-01
*	Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v	emakarov	2007-08-08
*	A generic preprocessing tactic zify for (r)omega	letouzey	2007-07-18
*	Mise en forme des theories	notin	2006-10-17
*	ajout de QArith dans les theories standards	letouzey	2006-05-31
*	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
*	Report de lemmes de Znumtheory dans Zabs ou BinInt	herbelin	2003-11-29
*	ajout Pnat (suite)	herbelin	2003-11-21
*	cosmetique	herbelin	2003-11-14
*	Restructuration ZArith	herbelin	2003-11-12