coq - The formal proof system

Age	Commit message (Expand)	Author
2007-05-10	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-13	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin
2006-12-12	MAJ	herbelin
2006-10-13	Correction test-suite suite à r9186	notin
2006-10-09	Exemple avec liaison des variables de filtrage du match	herbelin
2006-10-09	Notations:	herbelin
2006-09-25	Corrections mineures	notin
2006-09-23	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-06-09	Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...	herbelin
2006-05-28	Adaptation au passage de sig2 dans Type	herbelin
2006-05-10	Conformité nouveaux principes: Declare Module non utilisable pour définir u...	herbelin
2006-04-24	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin
2006-01-11	Ajout test notation récursive	herbelin
2006-01-05	Test choix conflit afficheur de nombres selon la présence ou pas d'une coercion	herbelin
2006-01-02	Affichage de 'O' (lettre) comme '0' (chiffre)	herbelin
2005-12-23	Test printing of Tactic Notation which was broken until dec 2005	herbelin
2005-12-22	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-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
2005-03-16	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin
2004-12-27	Ajout test bug 860	herbelin
2004-12-09	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-11-17	Test lieurs dans Notation	herbelin
2004-11-17	test-suite/output/Notations.out	herbelin
2004-06-02	Ajout tests affichage coercions vers Funclass	herbelin
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2003-10-10	* empty log message *	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-03-14	* empty log message *	barras
2003-03-04	MAJ	herbelin
2003-01-30	Pb de parenthèse dans "Check (S (plus O O))"	herbelin
2003-01-19	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin
2003-01-16	* empty log message *	herbelin
2003-01-15	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin
2003-01-09	Export M + Module M <: SIG	coq
2002-11-25	MAJ	herbelin
2002-11-24	MAJ	herbelin
2002-10-29	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin
2002-10-16	Parseur pour n>20 dans nat plus disponible	herbelin
2002-09-27	Encore quelques rangements dans Nametab + petits trucs	coq
2002-09-21	Changement de sémantique de Remark : maintenant un global comme les autres	herbelin