coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier	2014-10-01
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	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
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	Restore implicit arguments of irreflexivity (fixes bug #3305).	Matthieu Sozeau	2014-05-09
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	- Fix arity handling in retyping (de Bruijn bug!)	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Cbn is happier when ?SetPositive fixpoints have the set as recursive argument	Pierre Boutillier	2014-05-02
*	Eta contractions to please cbn	Pierre Boutillier	2014-05-02
*	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey	2013-07-17
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	MSetRBT: a tail-recursive plength	letouzey	2012-08-06
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	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
*	MSetAVL: better implementation of filter suggested by X. Leroy	letouzey	2012-01-17
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right	letouzey	2011-10-14
*	fsetdec : non-atomic elements are now transformed as variables first (fix #2464)	letouzey	2011-10-07
*	Improved handling of element equalities in fsetdec (fix #2467)	letouzey	2011-10-07
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey	2011-03-17
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	s/appartness/membership/g (Closes: #2470)	glondu	2011-01-06
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20
*	For the moment, two small manual eta-expansions to avoid '_a after extraction	letouzey	2010-09-17
*	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin	2010-07-22
*	MSetPositive: mention MSetInterface instead of FSetInterface	letouzey	2010-07-16
*	FSetPositive: sets of positive inspired by FMapPositive.	letouzey	2010-07-16
*	FSets/Msets: some renaming of module params to simplify the task of the extra...	letouzey	2010-07-05
*	Report fixes from FSetDecide to MSetDecide	letouzey	2010-06-18
*	MSetInterface: no induction principle about a Record (nicer extraction)	letouzey	2010-06-16
*	MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...	letouzey	2010-06-15
*	Made option "Automatic Introduction" active by default before too many	herbelin	2010-06-08
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Change definition of FSetList so that equality is Leibniz	glondu	2010-04-09
*	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey	2010-02-12
*	MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)	letouzey	2010-01-12
*	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey	2010-01-07