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
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Normalized type for Vector.map2	pboutill	2013-03-25
*	cbn friendly VectorDef	pboutill	2013-02-25
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Bugs revealed by playing with contribs	pboutill	2012-05-25
*	Vectors takes advantage of pattern matching compiler fixup	pboutill	2012-05-11
*	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
*	Less ambitious application of a notation for eq_rect. We proposed	herbelin	2011-08-10
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin	2011-07-16
*	As many notation for for vectors as for List.	pboutill	2011-05-03
*	- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...	msozeau	2011-03-23
*	Inference of match predicate produces ill-typed unification problem,	msozeau	2011-03-11
*	Vectors fully use implicit arguments	pboutill	2011-02-10
*	Fixpoints are traverse during implicits arguments search to toplevel	pboutill	2011-02-10
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	local variables can have implicits locally	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