coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction test-suite suite à r9186	notin	2006-10-13
*	Exemple avec liaison des variables de filtrage du match	herbelin	2006-10-09
*	Notations:	herbelin	2006-10-09
*	Corrections mineures	notin	2006-09-25
*	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin	2006-09-23
*	- Correction filtrage des notations impliquant un "match" : la présence	herbelin	2006-09-23
*	Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...	herbelin	2006-06-09
*	Adaptation au passage de sig2 dans Type	herbelin	2006-05-28
*	Conformité nouveaux principes: Declare Module non utilisable pour définir u...	herbelin	2006-05-10
*	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin	2006-04-24
*	Ajout test notation récursive	herbelin	2006-01-11
*	Test choix conflit afficheur de nombres selon la présence ou pas d'une coercion	herbelin	2006-01-05
*	Affichage de 'O' (lettre) comme '0' (chiffre)	herbelin	2006-01-02
*	Test printing of Tactic Notation which was broken until dec 2005	herbelin	2005-12-23
*	Abandon tests syntaxe v7 (correction)	herbelin	2005-12-22
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-22
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin	2005-03-16
*	Ajout test bug 860	herbelin	2004-12-27
*	Ajout d'une version nouvelle syntaxe	herbelin	2004-12-09
*	MAJ avec les particularités de l'afficheur v7 de la V8	herbelin	2004-12-09
*	Test d'affichage d'un Fix donné avec /n	herbelin	2004-12-09
*	Fichier non traductible (référence à des objets invisibles ce qui empêche...	herbelin	2004-12-09
*	Intégré à Implicit.v	herbelin	2004-12-09
*	Ajout suffixe 8 pour test en nouvelle syntaxe	herbelin	2004-12-09
*	Plus de statut spécial pour Remark	herbelin	2004-12-09
*	Désactivation du test du printer arithmétique v7	herbelin	2004-12-09
*	Test lieurs dans Notation	herbelin	2004-11-17
*	test-suite/output/Notations.out	herbelin	2004-11-17
*	Ajout tests affichage coercions vers Funclass	herbelin	2004-06-02
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	* empty log message *	herbelin	2003-10-10
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	* empty log message *	barras	2003-03-14
*	MAJ	herbelin	2003-03-04
*	Pb de parenthèse dans "Check (S (plus O O))"	herbelin	2003-01-30
*	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin	2003-01-19
*	* empty log message *	herbelin	2003-01-16
*	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin	2003-01-15
*	Export M + Module M <: SIG	coq	2003-01-09
*	MAJ	herbelin	2002-11-25
*	MAJ	herbelin	2002-11-24
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-29
*	Parseur pour n>20 dans nat plus disponible	herbelin	2002-10-16
*	Encore quelques rangements dans Nametab + petits trucs	coq	2002-09-27
*	Changement de sémantique de Remark : maintenant un global comme les autres	herbelin	2002-09-21
*	Correction	coq	2002-08-21
*	Test affichage optimal des coercions	herbelin	2002-08-14
*	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr	2002-06-21
*	Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output	herbelin	2002-06-07