coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-05-02	Cbn is happier when ?SetPositive fixpoints have the set as recursive argument	Pierre Boutillier
2014-05-02	Eta contractions to please cbn	Pierre Boutillier
2013-07-17	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-12-18	No more constant named "int" in Coq theories (cf bug #2878)	letouzey
2012-10-01	Ltac repeat is in fact already doing progress	letouzey
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2012-07-05	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-05-15	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey
2012-04-15	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin
2012-03-14	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau
2012-01-31	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau
2012-01-28	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
2011-10-14	MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right	letouzey
2011-10-07	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-05-05	Modularization of BinInt, related fixes in the stdlib	letouzey
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-02-17	- Use transparency information all the way through unification and	msozeau
2011-02-16	Fix compilation issues.	msozeau
2011-02-14	- Fix treatment of globality flag for typeclass instance hints (they	msozeau
2011-01-06	s/appartness/membership/g (Closes: #2470)	glondu
2010-12-17	Cosmetic : let's take advantage of the n-ary exists notation	letouzey
2010-10-22	FMapFacts: typo noticed by Aaron	letouzey
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-18	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin
2010-07-18	Tentative de suppression de l'import automatique des hints et coercions.	herbelin
2010-07-16	FSetPositive: sets of positive inspired by FMapPositive.	letouzey
2010-07-05	FSets/Msets: some renaming of module params to simplify the task of the extra...	letouzey
2010-06-18	fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...	letouzey
2010-06-17	fsetdec: clear dependent hypothesis before anything else (fix #2136).	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-02-12	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey
2010-01-07	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey
2010-01-07	Include can accept both Module and Module Type	letouzey
2009-12-09	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey
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-11-02	List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...	letouzey
2009-11-02	Remove various useless {struct} annotations	letouzey
2009-10-20	FSetCompat: a compatibility wrapper between FSets and MSets	letouzey
2009-10-19	Merge SetoidList2 into SetoidList.	letouzey
2009-10-16	Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...	letouzey
2009-10-13	MSets: a new generation of FSets	letouzey
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey