coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik	2017-06-01
*	Added take to VectorDef.	George Stelle	2017-03-30
*	Move vector/list compat notations to their relevant files	Jason Gross	2016-09-29
*	Remove spaces from around vector notations	Jason Gross	2016-09-26
*	Fix bug #4785 (use [ ] for vector nil)	Jason Gross	2016-09-26
*	Fixing bug #4684: Singleton list notation unusable in 8.5pl1.	Pierre-Marie Pédrot	2016-04-25
*	Emphasizing that eta for vectors is an instance of caseS, as pointed	Hugo Herbelin	2015-09-08
*	Adding a proof of eta on Vector.t of non-zero size.	Hugo Herbelin	2015-09-08
*	There was one more universe needed due to the use of now non-universe-polymor...	Matthieu Sozeau	2015-01-18
*	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
*	- 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
*	fixup complement Fin	Pierre Boutillier	2014-02-24
*	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey	2014-02-07
*	Nicer infered names in refine.	aspiwack	2013-11-04
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	Normalized type for Vector.map2	pboutill	2013-03-25
*	cbn friendly VectorDef	pboutill	2013-02-25
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Same for Fin	pboutill	2012-07-25
*	Vector equalities first stuff	pboutill	2012-07-20
*	Bugs revealed by playing with contribs	pboutill	2012-05-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
*	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