coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	All the parameters of or can be implicits.	pboutill	2011-07-26
*	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin	2011-07-16
*	Added a characterization of unique existence.	herbelin	2011-07-16
*	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
*	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin	2010-07-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Init/Logic: commutativity and associativity of /\ and \/	letouzey	2010-01-08
*	Implicit argument of Logic.eq become maximally inserted	letouzey	2009-10-08
*	Switched to "standardized" names for the properties of eq and	herbelin	2009-01-01
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.	emakarov	2007-11-08
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	Mise en forme des theories	notin	2006-10-17
*	Passage à une définition de inhabited plus dans les 'standard mathématique...	herbelin	2006-08-28
*	Modification déf de exists! pour éviter une éta-expansion et pouvoir être...	herbelin	2006-06-09
*	Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...	herbelin	2006-06-04
*	Ajout exists! et restructuration/extension des fichiers sur la	herbelin	2006-06-04
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	Titres moins envahissants pour coqdoc	herbelin	2006-03-04
*	Ajout 'exists! x:A, P (suite)	herbelin	2006-02-23
*	Ajout 'exists! x:A, P	herbelin	2006-02-23
*	code mort	herbelin	2006-02-10
*	Correction associativité de IF et exists (visible à l'affichage uniquement ...	herbelin	2006-01-19
*	Contrepartie de la suppression des boites automatiques dans format	herbelin	2005-12-22
*	Documentation	herbelin	2005-05-19
*	Nouvelle en-tête	herbelin	2004-07-16
*	Commentaires	herbelin	2004-03-29
*	MAJ Commentaires	herbelin	2004-02-28
*	Commentaires en v8	herbelin	2004-01-09
*	Finalement, espacement autour du ':' pour a la fois exists, forall et fun	herbelin	2003-12-23
*	Affichage sur le modèle du forall pour le exists	herbelin	2003-12-21
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Automatisation de la traduction de iff_trans; renommage IF	herbelin	2003-11-14
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Maintenant avant Datatypes	herbelin	2003-10-21
*	Des implicites plus 'naturels' pour eq_ind, identity_ind and co	herbelin	2003-10-17
*	Changement 'as notation' en 'where notation'	herbelin	2003-10-14
*	mise a jour nouvelle syntaxe	barras	2003-10-11
*	type_scope	herbelin	2003-10-10
*	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
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	Généralisation de l'utilisation de Notation	herbelin	2002-11-24
*	option -dump-glob pour coqdoc	filliatr	2002-02-14