coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	Grammar: "allowing to" is not proper English	Jason Gross	2014-08-25
*	More proofs independent of the names generated by induction/elim over	Hugo Herbelin	2014-08-05
*	Adding a generalized version of fold_Equal to FMapFacts.	Pierre Courtieu	2014-07-31
*	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond	2014-06-26
*	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau	2014-06-20
*	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
*	Fix after merge.	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
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	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-07-05
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau	2012-01-31
*	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau	2012-01-28
*	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
*	- 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
*	Fix compilation issues.	msozeau	2011-02-16
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	s/appartness/membership/g (Closes: #2470)	glondu	2011-01-06
*	Cosmetic : let's take advantage of the n-ary exists notation	letouzey	2010-12-17
*	FMapFacts: typo noticed by Aaron	letouzey	2010-10-22
*	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
*	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-18
*	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
*	fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...	letouzey	2010-06-18
*	fsetdec: clear dependent hypothesis before anything else (fix #2136).	letouzey	2010-06-17
*	Made option "Automatic Introduction" active by default before too many	herbelin	2010-06-08
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey	2010-02-12
*	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey	2010-01-07
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey	2009-12-09