coq - The formal proof system

Age	Commit message (Expand)	Author
2002-07-05	* empty log message *	corbinea
2002-07-05	Added a new uncompleteness bug found in Tauto.	corbinea
2002-06-14	* empty log message *	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context (2ème)	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context	herbelin
2002-06-11	Tests pour la tactique Reg	desmettr
2002-06-07	I added a comment on the tactic compute_POS.	bertot
2002-06-07	This example does not work in coq-7.3, but does in coq-7.2.	bertot
2002-06-06	Ajout exemple JCF conflit variable interne, variable de section	herbelin
2002-06-06	Des exemples sérieux	herbelin
2002-06-06	Ajout exemple Yves renommage différent d'une var de section	herbelin
2002-06-05	Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct	herbelin
2002-05-29	* empty log message *	herbelin
2002-02-28	* empty log message *	herbelin
2002-01-25	* empty log message *	herbelin
2002-01-21	Ajout test de Pierre Crégut	herbelin
2002-01-18	* empty log message *	herbelin
2002-01-18	* empty log message *	herbelin
2002-01-16	Ajout d'un test sur les anonymes dépendant dans des arguments implicites	herbelin
2002-01-15	Test le filtrage dépendant vers l'avant	herbelin
2001-12-21	* empty log message *	herbelin
2001-12-21	Ajout d'un exemple de Christine	herbelin
2001-12-19	MAJ Grammar	herbelin
2001-12-19	NatRing (2ème)	herbelin
2001-12-19	NatRing	herbelin
2001-12-19	Un peu plus d'inférence des ? traitée par le Cases	herbelin
2001-12-13	* empty log message *	herbelin
2001-12-11	Test des coercions dans les motifs	herbelin
2001-11-21	* empty log message *	herbelin
2001-11-21	La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...	herbelin
2001-11-21	Un bug dans le script	herbelin
2001-11-21	Sur la cumulativité dans les tactiques	herbelin
2001-11-21	Nouveaux exemples	herbelin
2001-11-20	* empty log message *	herbelin
2001-11-16	* empty log message *	herbelin
2001-11-08	Quelques tests sur le let-in	herbelin
2001-10-15	* empty log message *	herbelin
2001-10-15	Test compatibilité V6 pour les filtrages avec let-in	herbelin
2001-10-03	Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)	herbelin
2001-10-03	Tests de Cases avec définitions locales	herbelin
2001-10-01	Tests noms longs de modules	herbelin
2001-09-25	ajout d'un fichier test pour setoides	clrenard
2001-09-21	Vérification de la syntaxe des options	herbelin
2001-09-20	Test inférence prédicat en présence d'univers	herbelin
2001-09-20	Refine et let-in	filliatr
2001-09-19	Quelques signes extérieurs de la sémantique de Remark, question visibilité	herbelin
2001-09-19	Ces fichiers décrivent des comportements peut-être souhaités mais actuelle...	herbelin
2001-09-13	Syntaxe des Hints	herbelin
2001-06-25	Bug inférence du prédicat en présence de K-rédex	herbelin
2001-06-15	Fix d'un bug de Tauto	delahaye