coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
*	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	ZArith/Int.v: some modernizations	Pierre Letouzey	2015-04-02
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	"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
*	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
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey	2011-03-17
*	- 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
*	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
*	MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)	letouzey	2010-01-12
*	MSetAVL: hints made local since some of them are quite violent (transitivity)	letouzey	2010-01-07
*	Avoid declaring hints about refl/sym/trans of eq in DecidableType2	letouzey	2010-01-05
*	Fix [Instance: forall ..., C args := t] declarations to behave as	msozeau	2009-11-15
*	Use generalizable variables info when internalizing arbitrary bindings,	msozeau	2009-11-08
*	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-03
*	OrderedType2 : trivial lemmas are turned into tests for order.	letouzey	2009-10-16
*	MSets: a new generation of FSets	letouzey	2009-10-13