coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-11	Modify Vectors/Fin.v to compile with -mangle-names	Jasper Hugunin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	Fixing typos - Part 3	JPR
2018-02-27	Update headers following #6543.	Théo Zimmermann
2015-09-08	Emphasizing that eta for vectors is an instance of caseS, as pointed	Hugo Herbelin
2014-07-22	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-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-02-24	fixup complement Fin	Pierre Boutillier
2014-02-07	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-07-25	Same for Fin	pboutill
2012-05-11	Vectors takes advantage of pattern matching compiler fixup	pboutill
2012-05-02	Coqide highligthing is back (done by gtksourceview).	pboutill
2012-03-14	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau
2012-02-29	Vector: missing injection lemmas and better impossible branches	pboutill
2011-12-07	Vectors use a bit more the pattern matching compiler	pboutill
2011-11-21	VectorDef.v takes benefit of dependencies being taken into account	herbelin
2011-02-10	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
2010-12-10	First release of Vector library.	pboutill