coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	No more Coersion in Init.	Pierre Boutillier	2014-04-10
*	Define [projT3] and [proj3_sig]	Jason Gross	2014-04-10
*	Better unification for [projT1] and [proj1_sig].	Jason Gross	2013-12-12
*	Relaxing the constraint on eta-expanding on the fly while looking for	herbelin	2013-05-05
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Updating headers.	herbelin	2012-08-08
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Bug 2767	pboutill	2012-05-09
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Same Implicit Arguments rule for sumbool and sumor.	pboutill	2011-07-26
*	Init: some results in Type should rather be Defined than Qed	letouzey	2011-03-21
*	Used multiple lists of implicit arguments to transfer the choices of	herbelin	2010-10-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Some lemmas about dependent choice + extensions of Compare_dec +	herbelin	2009-11-16
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	MAJ et bricoles diverses	herbelin	2008-05-12
*	Une passe sur les réels:	herbelin	2008-03-23
*	Ajout exist & cie à la table des hints par symétrie avec ex_intro &	herbelin	2007-06-22
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	Documentation	herbelin	2005-05-19
*	Nouvelle en-tête	herbelin	2004-07-16
*	sumbool et sumor affich avec 'if' si possible	herbelin	2004-04-06
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Passage des notations de type dans type_scope	herbelin	2003-10-28
*	Commentaires	herbelin	2003-10-23
*	Argument de except, error implicite seulement en v8; Changement 'as notation'...	herbelin	2003-10-14
*	Argument implicite pour None, error, except	herbelin	2003-10-13
*	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...	herbelin	2003-09-23
*	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin	2003-05-21
*	Activation des implicites pour la v8	herbelin	2003-04-09
*	Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiques	herbelin	2002-11-26
*	Retablissement SynDef Value/Error	herbelin	2002-11-25
*	Généralisation de l'utilisation de Notation	herbelin	2002-11-24
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring	2002-01-31
*	MAJ des Id pour coqweb	herbelin	2002-01-09
*	Suppression d'Export redondants	herbelin	2001-11-14
*	and_rec redondant	letouzey	2001-09-27
*	Fin de la modif Exc/option	mohring	2001-08-30
*	ajout option , Exc --> option, et lemmes dans les theories	mohring	2001-08-29
*	Expérimentation de NewDestruct et parfois NewInduction	herbelin	2001-08-05
*	documentation automatique de la bibliothèque standard	filliatr	2001-04-11
*	Introduction d'une preuve de False_rec	mohring	2001-03-30
*	entetes	filliatr	2001-03-15