coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	modification de la definition des def inductives unitaires et autorisation d'...	mohring	2002-01-29
*	MAJ des Id pour coqweb	herbelin	2002-01-09
*	Suppression d'Export redondants	herbelin	2001-11-14
*	Transparent	barras	2001-09-20
*	ajout option , Exc --> option, et lemmes dans les theories	mohring	2001-08-29
*	Expérimentation de NewDestruct et parfois NewInduction	herbelin	2001-08-05
*	entetes	filliatr	2001-03-15
*	separation calcul des implicites et declaration des constantes / inductifs / ...	filliatr	2000-11-21
*	fichiers prelude Coq	filliatr	1999-12-13