coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-16	add results on to_list	Olivier Laurent
2020-11-16	Explicitly annotate all hint declarations of the standard library.	Pierre-Marie Pédrot
2020-10-11	Modify Vectors/VectorEq.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Vectors/VectorSpec.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Vectors/VectorDef.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Vectors/Fin.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-20	Fix coqdoc title: should be on a single line.	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-12-19	Put #[universes(template)] on all auto template spots in stdlib	Gaëtan Gilbert
2018-11-14	Deprecate hint declaration/removal with no specified database	Maxime Dénès
2018-10-17	Strings: add ByteVector	Yishuai Li
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
2018-07-30	Vector: expose ++ to user	Yishuai Li
2018-03-05	Merge PR #6855: Update headers following #6543.	Maxime Dénès
2018-03-02	Remove VOld compatibility flag.	Théo Zimmermann
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin
2017-06-01	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik
2017-03-30	Added take to VectorDef.	George Stelle
2016-09-29	Move vector/list compat notations to their relevant files	Jason Gross
2016-09-26	Remove spaces from around vector notations	Jason Gross
2016-09-26	Fix bug #4785 (use [ ] for vector nil)	Jason Gross
2016-04-25	Fixing bug #4684: Singleton list notation unusable in 8.5pl1.	Pierre-Marie Pédrot
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-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	- 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-02-24	fixup complement Fin	Pierre Boutillier
2014-02-07	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey
2013-11-04	Nicer infered names in refine.	aspiwack
2013-11-02	A whole new implemenation of the refine tactic.	aspiwack
2013-03-25	Normalized type for Vector.map2	pboutill
2013-02-25	cbn friendly VectorDef	pboutill
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-07-25	Same for Fin	pboutill
2012-07-20	Vector equalities first stuff	pboutill
2012-05-25	Bugs revealed by playing with contribs	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