coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nouvelle en-tête	herbelin	2004-07-16
*	Definition de la notation de la paire par un motif recursif	herbelin	2004-03-17
*	Duplication temporaire des règles de syntaxe des paires	herbelin	2003-12-16
*	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
*	Ajout lemme projections	herbelin	2003-11-12
*	Passage de la notations de paire dans core_scope	herbelin	2003-10-28
*	ajouts	herbelin	2003-10-21
*	Des implicites plus 'naturels' pour eq_ind, identity_ind and co	herbelin	2003-10-17
*	Argument de None implicite seulement en v8	herbelin	2003-10-14
*	Argument implicite pour None, error, except	herbelin	2003-10-13
*	identity est equivalent sur Type (sauf sans argument)	herbelin	2003-10-10
*	Delimiters N devient 'nat'	herbelin	2003-10-10
*	traducteur: affiche les commentaires a l'interieur des commandes	barras	2003-09-22
*	Nettoyage	herbelin	2003-09-21
*	Bind et Delimit pour nat	herbelin	2003-09-12
*	Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...	herbelin	2003-09-11
*	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin	2003-05-21
*	Intégration DatatypesSyntax à Datatypes	herbelin	2003-04-17
*	Activation des implicites pour la v8	herbelin	2003-04-09
*	Généralisation de l'utilisation de Notation	herbelin	2002-11-24
*	Doc	herbelin	2002-02-22
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	MAJ des Id pour coqweb	herbelin	2002-01-09
*	ajout option , Exc --> option, et lemmes dans les theories	mohring	2001-08-29
*	entetes	filliatr	2001-03-15
*	fichiers prelude Coq	filliatr	1999-12-13