coq - The formal proof system

Age	Commit message (Expand)	Author
2008-11-27	added tests for hyps reordering	barras
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-25	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin
2008-04-22	fixed universes bug related to module inclusion	barras
2008-04-21	test module include w.r.t. universe constraints	barras
2007-10-16	Vérification que "rewrite in" se comporte comme "rewrite" et échoue	herbelin
2007-09-06	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin
2007-02-21	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran
2007-01-19	Tests de référence circulaire au sous-typage de module (pour mémoire)	herbelin
2007-01-17	Correction bug #1302	herbelin
2006-12-13	test condition de garde	barras
2006-10-27	Check that sort-polymorphic inductive types is not too lax	herbelin
2006-10-27	Cette dérivation de paradoxe passait en V8.1beta	herbelin
2006-10-13	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin
2006-08-22	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest
2006-06-23	Stricte positivité en présence de types inductifs imbriqués avec paramètr...	herbelin
2006-06-22	Deux vérifications que le polymorphisme de sorte des inductifs ne fonctionne...	herbelin
2006-05-13	Correction trou de typage des éliminations d'inductifs introduit dans commit...	herbelin
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
2005-12-21	cf ltac4.v	herbelin
2005-11-03	deplacement params_ind	mohring
2004-11-17	test-suite/output/Notations.out	herbelin
2004-10-17	* empty log message *	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2003-12-17	ajout test de non-regression Clear d'une def locale	barras
2003-10-10	Cacher les .v8	herbelin
2003-09-23	test d'implicite incorrect depuis que eq porte sur Type	barras
2003-01-20	* empty log message *	herbelin
2003-01-19	Tests ltac	herbelin
2002-08-15	Test for redundant clauses	herbelin
2002-06-07	Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output	herbelin
2002-04-12	* empty log message *	herbelin
2001-11-21	* empty log message *	herbelin
2001-11-21	Sur l'exahustivité du filtrage	herbelin
2001-10-17	Test soumis par Randy Pollack	herbelin
2001-10-05	Test de dépendances de ClearBody	herbelin
2001-09-19	Quelques signes extérieurs de la sémantique de Remark, question visibilité	herbelin
2001-09-09	Tests l'incohérence des univers	herbelin
2001-04-25	MAJ	herbelin
2001-04-20	Erreurs de Cases	mohring
2001-04-20	Ajout d'erreurs sur le Case avec branche redondante	mohring
2001-04-13	ajout de tests	mohring
2001-03-15	entetes	filliatr
2001-03-14	* empty log message *	herbelin
2001-02-05	Pas d'Apply dans Tauto	delahaye
2001-02-05	Ajout du test de Tauto	delahaye
2000-12-12	Ajout de tests	mohring
2000-12-09	tests automatiques	herbelin