coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	Noms de compatibilité déplacés en bloc à la fin du fichier	herbelin	2006-10-26
*	Ménage	notin	2006-10-25
*	oops	barras	2006-10-25
*	conflit de nom (Field_theory) modulo la casse	barras	2006-10-25
*	Correction sym -> comm	herbelin	2006-10-19
*	typo doc + bug legacy field	barras	2006-10-16
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Exploitation du 'let rec' + présentation	herbelin	2006-03-05
*	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
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin	2005-12-26
*	Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...	herbelin	2005-12-21
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	Nouvelle en-tête	herbelin	2004-07-16
*	reals: renamed type option into field_rel_option	marche	2004-03-11
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	petits changements de syntaxe	barras	2003-11-12
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Cacher les .v8	herbelin	2003-10-03
*	Ajout fonctions syntaxe v8 pour contrib MapleMode	herbelin	2003-09-23
*	Système de renommage des noms de tactiques Ltac	herbelin	2003-09-22
*	Passage à la V8 par défaut	herbelin	2003-09-22
*	Pour accomoder autant le printer v8 que v7	herbelin	2003-09-06
*	Protection contre les types sans corps associé	herbelin	2003-09-06
*	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
*	Explicitation arguments de eq	herbelin	2003-04-11
*	Mauvaise resolution conflit dans commit precedent	herbelin	2003-04-07
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Légères simplifications code de Field; message d'erreur si pas égalité	herbelin	2003-04-03
*	remplace == par = dans la tactique field pour que le debugger marche a nouvea...	narboux	2003-04-01
*	Fail 1 pour traverser le match	herbelin	2003-04-01
*	Plus de eqT; message Fail	herbelin	2003-03-31
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
*	* empty log message *	barras	2003-03-12
*	Utilisation de 'Recursive' pour les tactiques récursives	herbelin	2003-01-20
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	MAJ syntaxe	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin	2002-06-03
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
*	Fix d'un bug sur le test des inverses	delahaye	2002-03-19
*	Meilleure gestion de la reduction dans Field	delahaye	2002-03-17