coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Oubli d'un quote	herbelin	2001-12-18
*	oubli: changement de nil en nilT	mayero	2001-11-14
*	Changement de list en listT, cons en consT et app en appT	mayero	2001-11-14
*	GROS COMMIT:	barras	2001-11-05
*	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye	2001-10-23
*	Correction due au changement de semantique de Match	delahaye	2001-09-21
*	Transparent	barras	2001-09-20
*	Parsing	herbelin	2001-08-10
*	Ajout d'un Ring pour setoides	clrenard	2001-07-10
*	Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...	herbelin	2001-07-02
*	Reduction du terme preuve fourni par Field	delahaye	2001-06-27
*	Reduction tres significative du terme preuve	delahaye	2001-06-27
*	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin	2001-06-25
*	Changement de la structure des points fixes	barras	2001-05-03
*	Suppression d'une partie de code commente	delahaye	2001-04-24