coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin	2013-03-21
*	Updating headers.	herbelin	2012-08-08
*	Numbers: some improvements in proofs	letouzey	2011-01-03
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Support "Local Obligation Tactic" (now the default in sections).	msozeau	2010-01-11
*	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
*	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau	2009-09-15
*	- Implementation of a new typeclasses eauto procedure based on success	msozeau	2009-04-27
*	Rename [Morphism] into [Proper] and [respect] into [proper] to comply	msozeau	2009-04-21
*	Use manual implicts in Classes and rationalize class parameter names.	msozeau	2008-09-14
*	Enhanced discrimination nets implementation, which can now work with	msozeau	2008-06-27
*	- Cleanup parsing of binders, reducing to a single production for all	msozeau	2008-05-11
*	Fixes in new Morphisms files.	msozeau	2008-04-09
*	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau	2008-04-08