coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suppression de la partie ML de la contrib correctness. Les fichiers	herbelin	2008-04-29
*	Correction du bug des types singletons pas sous-type de Set	herbelin	2008-04-27
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	useless Require Export Extraction	letouzey	2007-11-06
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	Generalized CAMLP4USE for pp dependencies	corbinea	2007-07-16
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Traduction des noms v7 en noms v8	herbelin	2005-12-25
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	Nouvelle en-tête	herbelin	2004-07-16
*	bugs avec Pose et Assert	barras	2004-01-09
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Parenthesage du terme pour accepter 'of' comme non ident	herbelin	2003-12-24
*	'of' restait par erreur mot-cle dans psyntax.ml4 en v8	herbelin	2003-12-23
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Remplacement de l'indicateur de date "@" par 'at'	herbelin	2003-11-26
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Prise en compte renommages	herbelin	2003-11-19
*	Correction chemin de Z	herbelin	2003-11-14
*	traduction des noms de correctness	herbelin	2003-10-30
*	Affichage des buts par Pfedit pour utilisation par les tactiques	herbelin	2003-10-10
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Cacher les .v8	herbelin	2003-10-03
*	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin	2003-09-23
*	Indépendance vis à vis de Declare	herbelin	2003-09-12
*	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin	2003-09-06
*	Traducteur de correctness	herbelin	2003-08-14
*	code mort	herbelin	2003-08-14
*	Notation access au dessous du niveau applicatif (2eme)	herbelin	2003-08-14
*	Notation access au dessous du niveau applicatif	herbelin	2003-08-13
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Divers	herbelin	2003-04-17
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	* Ajout du traducteur nouvelle syntaxe *	barras	2003-03-12
*	Evaluation paresseuse de l'affichage du debug	herbelin	2002-12-15
*	Compensation de suppression betaiota de type_of	herbelin	2002-12-11
*	Normalisation des types (fait avant dans Typing)	herbelin	2002-12-10
*	Court-circuit de g_zsyntax	herbelin	2002-11-28
*	Remplacement Grammar/Syntax par Notation	herbelin	2002-11-26
*	typo	herbelin	2002-11-18