coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier	2014-10-01
*	MSetRBT: unfortunate typo in compare_height (fix #3413)	Pierre Letouzey	2014-07-10
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond	2014-06-26
*	- 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
*	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey	2013-07-17
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	MSetRBT: a tail-recursive plength	letouzey	2012-08-06
*	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-07-05
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13