coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Documentation Prop<=Set et Arguments Scope Global	herbelin	2008-07-01
*	Renommage id dans le test Nametab (suite ajout d'une constante de ce	herbelin	2008-06-05
*	Petites corrections vis à vis des commits 10860, 10859, 10850	herbelin	2008-04-28
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Diverses petites modifs dans la test-suite:	notin	2008-03-26
*	Correction de bugs relatifs a la compostion des substitutions	soubiran	2008-03-25
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
*	Beaoucoup de changements dans la representation interne des modules.	soubiran	2008-02-01
*	Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)	notin	2008-01-22
*	Correction de quelques défauts d'affichage (notations sous "as" pour	herbelin	2007-10-05
*	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin	2007-09-21
*	removed thesis	barras	2007-07-23
*	Update (test-suite was not successful).	glondu	2007-07-12
*	Factorisation des paramètres dans l'affichage des inductifs	herbelin	2007-07-02
*	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin	2007-05-10
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin	2007-04-13
*	MAJ	herbelin	2006-12-12
*	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