coq - The formal proof system

Age	Commit message (Expand)	Author
2006-08-17	Checks that abstract setoid rings can be defined in a module and the tactic	bertot
2006-07-07	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin
2006-07-04	functional inversion now takes a quatified hypothesis as first argument	jforest
2006-07-04	- completely new version of "functional inversion" using inversion on	jforest
2006-07-03	Test des motifs disjonctifs multiples	herbelin
2006-06-27	Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...	herbelin
2006-06-23	modifs de test-suite suite au passage des graphes de Function dans Type	jforest
2006-06-06	+ ameliorating the tactic "functional induction"	jforest
2006-05-31	Fusion if.v et If.v (MacOS X ne sait pas distinguer la casse)	herbelin
2006-05-31	Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casse	herbelin
2006-05-28	Adaptation au passage de vector dans Type	herbelin
2006-05-28	Adaptation au passage de option dans Type	herbelin
2006-05-22	encore un exemple ne marchant pas, ni avec omega ni avec romega	letouzey
2006-05-19	tests de Romega	letouzey
2006-05-10	Centralisation de la détection lettre/symbole par le lexeur dans les plages ...	herbelin
2006-05-05	Vieux bug de fin 2004 gardé pour mémoire	herbelin
2006-04-28	Ajout bug #1102	herbelin
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-04-15	Tests notations	herbelin
2006-03-22	- Correction bug calcul mind_consnrealargs, introduit à la révision	herbelin
2006-03-05	Ajout test relatif au bug #984	herbelin
2006-03-02	Ajout test bug 1089	herbelin
2006-03-02	Correction du bug 808: il est maintenant interdit de déclarer une assomption...	coq
2006-03-01	Correction bug #842 (rename d'une hyp du contexte)	herbelin
2006-01-30	Prise en compte coercions autour des sous-termes filtrés (si non dépendants)	herbelin
2006-01-23	Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...	herbelin
2006-01-20	Test bug 983	herbelin
2006-01-15	Test utf-8	herbelin
2006-01-11	Test conflictuel - ajouté pour mémoire	herbelin
2006-01-11	Test or-patterns	herbelin
2005-12-30	Test bug #1025	herbelin
2005-12-27	Mini-test d'extraction	herbelin
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
2005-12-21	Activation du test de Refine en v7 pour mémoire avant passage à la v8	herbelin
2005-11-03	* empty log message *	mohring
2005-11-02	Test reproductibilité du bug #1031	herbelin
2005-09-09	Declare Implicit Tactic	herbelin
2005-09-09	Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...	herbelin
2005-09-08	Test clear final dans intros pattern	herbelin
2005-05-19	A wish by Bas Spitters granted: a little more of unification up to	sacerdot
2005-05-18	Implemented autorewrite with ... in hyp [using ...].	sacerdot
2005-03-21	Ajout Unset Implicit Arguments manquant	herbelin
2005-03-20	Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...	herbelin
2005-03-19	Ajout test bug #935	herbelin
2005-03-17	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin
2005-03-16	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin
2005-03-08	Fix bug #931: leave dependent evars as such for refine	herbelin
2005-02-21	* empty log message *	herbelin
2005-02-17	Test bug #922	herbelin
2005-02-02	test de la bonne position des vars de ltac entre les vars et les rels	herbelin