coq - The formal proof system

Age	Commit message (Expand)	Author
2013-07-17	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey
2012-12-18	No more constant named "int" in Coq theories (cf bug #2878)	letouzey
2012-10-26	Change Hint Resolve, Immediate to take a global reference as argument	msozeau
2012-04-13	MSetRBT : implementation of MSets via Red-Black trees	letouzey
2012-01-17	MSetAVL: better implementation of filter suggested by X. Leroy	letouzey
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
2011-05-05	Modularization of BinInt, related fixes in the stdlib	letouzey
2011-03-17	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey
2011-02-17	- Use transparency information all the way through unification and	msozeau
2011-01-06	s/appartness/membership/g (Closes: #2470)	glondu
2010-09-20	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey
2010-09-17	For the moment, two small manual eta-expansions to avoid '_a after extraction	letouzey
2010-07-22	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin
2010-06-15	MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...	letouzey
2010-06-08	Made option "Automatic Introduction" active by default before too many	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-01-12	MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)	letouzey
2010-01-07	MSetAVL: hints made local since some of them are quite violent (transitivity)	letouzey
2010-01-05	Avoid declaring hints about refl/sym/trans of eq in DecidableType2	letouzey
2009-11-15	Fix [Instance: forall ..., C args := t] declarations to behave as	msozeau
2009-11-08	Use generalizable variables info when internalizing arbitrary bindings,	msozeau
2009-11-03	Better visibility of the inductive CompSpec used to specify comparison functions	letouzey
2009-11-03	OrderedType implementation for various numerical datatypes + min/max structures	letouzey
2009-10-16	OrderedType2 : trivial lemmas are turned into tests for order.	letouzey
2009-10-13	MSets: a new generation of FSets	letouzey