coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	Eta contractions to please cbn	Pierre Boutillier	2014-05-02
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	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
*	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
*	MSets: a new generation of FSets	letouzey	2009-10-13