coq - The formal proof system

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