coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-18	Support locality attributes for Hint Rewrite (including export)	Gaëtan Gilbert
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-09-03	New lemmas for List.v	Oliver Nash
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-25	Modifying theories to preferably use the "[= ]" syntax, and,	Hugo Herbelin
2018-11-14	Deprecate hint declaration/removal with no specified database	Maxime Dénès
2018-02-27	Update headers following #6543.	Théo Zimmermann
2016-06-18	Giving a more natural semantics to injection by default.	Hugo Herbelin
2014-10-01	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier
2014-07-10	MSetRBT: unfortunate typo in compare_height (fix #3413)	Pierre Letouzey
2014-07-09	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey
2014-06-26	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond
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
2013-07-17	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey
2012-10-26	Change Hint Resolve, Immediate to take a global reference as argument	msozeau
2012-08-06	MSetRBT: a tail-recursive plength	letouzey
2012-07-05	MSetRBT : elementary arith proofs instead of calls to lia	letouzey
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-04-13	MSetRBT : implementation of MSets via Red-Black trees	letouzey