coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Typeclasses: stdlib fixes for new search algorithm	Matthieu Sozeau	2016-06-16
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	Qcanon : implement some old suggestions by C. Auger	Pierre Letouzey	2016-02-26
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	Fixing bug #3270. Patch by Robbert Krebbers.	Pierre-Marie Pédrot	2014-07-08
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	More dynamic argument scopes	letouzey	2013-07-17
*	Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)	letouzey	2012-12-18
*	Updating headers.	herbelin	2012-08-08
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Zcompare.destr_zcompare subsumed by case Z.compare_spec	letouzey	2011-06-20
*	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey	2011-06-20
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey	2011-03-17
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	BigQ : setting correct arguments scopes	letouzey	2011-02-23
*	First release of Vector library.	pboutill	2010-12-10
*	Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits	letouzey	2010-11-18
*	Numbers: new functions pow, even, odd + many reorganisations	letouzey	2010-10-14
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made option "Automatic Introduction" active by default before too many	herbelin	2010-06-08
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	More improvements of BigN, BigZ, BigQ:	letouzey	2010-01-18
*	BigN, BigZ, BigQ: presentation via unique module with both ops and props	letouzey	2010-01-17
*	RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd	letouzey	2009-12-18
*	Fix anomaly when using typeclass resolution with filtered hyps in evars.	msozeau	2009-12-06
*	Fix backtracking heuristic in typeclass resolution.	msozeau	2009-11-30
*	BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)	letouzey	2009-11-12
*	Repair interpretation of numeral for BigQ, add a printer (close #2160)	letouzey	2009-11-12
*	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
*	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
*	Fix bug #1899: no more strange notations for Qge and Qgt	letouzey	2008-07-04
*	QMake : alternative equivalences with Qcanon thanks to earlier irreducibility...	letouzey	2008-06-30
*	QMake: Proofs that add_norm and other ..._norm functions produce irreducible ...	letouzey	2008-06-28
*	Some work on BigQ :	letouzey	2008-06-25
*	BigQ: starting to create and use an interface QSig	letouzey	2008-06-01
*	Enhance the BigN and BigZ infrastructure:	letouzey	2008-06-01
*	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
*	Integration of theories/Ints into theories/Numbers, part 1: moving files	letouzey	2008-05-07