coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)	letouzey	2012-12-18
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	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
*	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey	2010-02-12
*	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
*	GenericMinMax: still a min_case_strong with hypothesis in the wrong order	letouzey	2010-01-12
*	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey	2010-01-07
*	Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...	letouzey	2010-01-07
*	misc improvements in some Structures files	letouzey	2010-01-07
*	Avoid declaring hints about refl/sym/trans of eq in DecidableType2	letouzey	2010-01-05
*	Reverse order of arguments in min_case_strong for better uniformity (and comp...	letouzey	2009-12-17
*	OrderedType implementation for various numerical datatypes + min/max structures	letouzey	2009-11-03