coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-16	add results on to_list	Olivier Laurent
2020-10-11	Modify Vectors/VectorSpec.v to compile with -mangle-names	Jasper Hugunin
2020-04-11	add properties of operations on vectors	Olivier Laurent
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-09-01	edits per review	Yishuai Li
2019-09-01	Vectors: lemmas about uncons and splitAt	Yishuai Li
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-03-30	Added take to VectorDef.	George Stelle
2015-09-08	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-01-18	There was one more universe needed due to the use of now non-universe-polymor...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-11-04	Nicer infered names in refine.	aspiwack
2013-11-02	A whole new implemenation of the refine tactic.	aspiwack
2012-07-20	Vector equalities first stuff	pboutill
2012-02-29	Vector: missing injection lemmas and better impossible branches	pboutill
2011-02-10	Vectors fully use implicit arguments	pboutill
2010-12-10	First release of Vector library.	pboutill