coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Simplified rect2, it turns out Arthur's trick was not required.	Maxime Dénès	2014-07-22
*	A version of Fin.rect2 that is compatible with the fix of the guard condition.	Maxime Dénès	2014-07-22
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	fixup complement Fin	Pierre Boutillier	2014-02-24
*	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey	2014-02-07
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Same for Fin	pboutill	2012-07-25
*	Vectors takes advantage of pattern matching compiler fixup	pboutill	2012-05-11
*	Coqide highligthing is back (done by gtksourceview).	pboutill	2012-05-02
*	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau	2012-03-14
*	Vector: missing injection lemmas and better impossible branches	pboutill	2012-02-29
*	Vectors use a bit more the pattern matching compiler	pboutill	2011-12-07
*	VectorDef.v takes benefit of dependencies being taken into account	herbelin	2011-11-21
*	Vectors fully use implicit arguments	pboutill	2011-02-10
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	First release of Vector library.	pboutill	2010-12-10