coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove deprecated options from the standard library.	Guillaume Melquiond	2017-06-14
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Put implicits back as in 8.4.	Matthieu Sozeau	2015-12-31
*	Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)	Guillaume Melquiond	2015-05-12
*	Update headers.	Maxime Dénès	2015-01-12
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Give the same argument name for the record binder of type class	Matthieu Sozeau	2014-10-10
*	Restore implicit arguments of irreflexivity (fixes bug #3305).	Matthieu Sozeau	2014-05-09
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Updating headers.	herbelin	2012-08-08
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...	letouzey	2011-10-05
*	StrictOrder marked explicitly to be in Prop	letouzey	2011-07-04
*	Add [Typeclasses Debug] option that respects backtracking, solve	msozeau	2011-01-11
*	In passing, very quick uniformization of coqdoc headers in a few files.	herbelin	2010-12-09
*	Minor fixes:	msozeau	2010-07-27
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	RelationClasses: adapt eq_Reflexive and co to avoid Universe Inconsistencies	letouzey	2010-02-17
*	ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType	letouzey	2010-02-09
*	Support "Local Obligation Tactic" (now the default in sections).	msozeau	2010-01-11
*	Use generalizable variables info when internalizing arbitrary bindings,	msozeau	2009-11-08
*	list, length, app are migrated from List to Datatypes	letouzey	2009-11-02
*	Add a new vernacular command for controling implicit generalization of	msozeau	2009-10-27
*	Fix new instances that could easily make class resolution loop on	msozeau	2009-10-22
*	MSets: a new generation of FSets	letouzey	2009-10-13
*	Correctly do backtracking during type class resolution even if only new	msozeau	2009-10-05
*	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey	2009-09-28
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau	2009-09-15
*	Misc fixes:	msozeau	2009-09-10
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	Minor fixes in typeclasses:	msozeau	2009-05-16
*	- Implementation of a new typeclasses eauto procedure based on success	msozeau	2009-04-27
*	Better Requires in Classes. Fix bug #2093: the code does not require	msozeau	2009-04-16
*	Move setoid_rewrite to its own module and do some clean up in	msozeau	2009-04-07
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Fix [subrelation] clauses that privileged the weakest. Better impl args	msozeau	2009-02-04
*	Last changes in type class syntax:	msozeau	2009-01-18
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Use manual implicts in Classes and rationalize class parameter names.	msozeau	2008-09-14