coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	make validate repaired via a temporary fix for #2949	letouzey	2013-02-13
*	Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)	letouzey	2012-12-18
*	Updating headers.	herbelin	2012-08-08
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	Numbers: some improvements in proofs	letouzey	2011-01-03
*	Add sqrt in Numbers	letouzey	2010-10-19
*	Numbers : also axiomatize constants 1 and 2.	letouzey	2010-10-14
*	Numbers: new functions pow, even, odd + many reorganisations	letouzey	2010-10-14
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin	2010-07-18
*	Tentative de suppression de l'import automatique des hints et coercions.	herbelin	2010-07-18
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	BigN, BigZ, BigQ: presentation via unique module with both ops and props	letouzey	2010-01-17
*	Simplification of OrdersTac thanks to the functor application ! with no inline	letouzey	2010-01-17
*	Avoid some more re-declarations of Equivalence instances	letouzey	2010-01-14
*	NZAxioms plus a compare allows to build an OrderedType	letouzey	2010-01-08
*	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey	2010-01-07
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	Numbers: separation of funs, notations, axioms. Notations via module, without...	letouzey	2010-01-07
*	Numbers abstract layer: more Module Type, used especially for divisions.	letouzey	2010-01-05
*	NZDomain: investigation of the shape of NZ domain, more results about ofnat:n...	letouzey	2009-12-10
*	Diamond-shape instead of linear hiearchy in Numbers/NatInt	letouzey	2009-11-18
*	Simplification of Numbers, mainly thanks to Include	letouzey	2009-11-10
*	Numbers: more (syntactic) changes toward new style of type classes	letouzey	2009-11-06
*	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey	2009-10-08
*	Uniformity with the rest of the StdLib : _symm --> _sym	letouzey	2008-12-12
*	In abstract parts of theories/Numbers, plus/times becomes add/mul,	letouzey	2008-06-03
*	switch theories/Numbers from Set to Type (both the abstract and the bignum pa...	letouzey	2008-05-22
*	Coq headers + $ in theories/Numbers files	letouzey	2008-05-15
*	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau	2008-03-07
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	An update on Numbers. Added two files dealing with recursion, for information...	emakarov	2007-11-22
*	Added theorems; created NZPlusOrder from NTimesOrder.	emakarov	2007-11-16
*	Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder...	emakarov	2007-11-14
*	Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.	emakarov	2007-11-08
*	Replaced BinNat with a new version that is based on theories/Numbers/Natural/...	emakarov	2007-11-07
*	An update of theories/Numbers	emakarov	2007-11-03
*	Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu...	emakarov	2007-10-23
*	Added transitivity and irreflexivity of <, as well as < -elimination for bina...	emakarov	2007-10-16
*	Added the compilation of theories/Numbers to Makefile.common. The following t...	emakarov	2007-10-01
*	Update on theories/Numbers. Natural numbers are mostly complete,	emakarov	2007-09-21