coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Extension et réorganisation de l'interprétation des (co-)points fixes	herbelin	2006-09-01
*	Diverses modifications autour de l'unification modulo conversion:	herbelin	2006-08-28
*	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest	2006-08-22
*	remove an orphan comment (attached to a piece of code that was removed).	bertot	2006-08-22
*	Checks that abstract setoid rings can be defined in a module and the tactic	bertot	2006-08-17
*	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin	2006-07-07
*	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-04
*	Test des motifs disjonctifs multiples	herbelin	2006-07-03
*	Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...	herbelin	2006-06-27
*	modifs de test-suite suite au passage des graphes de Function dans Type	jforest	2006-06-23
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
*	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-31
*	Adaptation au passage de vector dans Type	herbelin	2006-05-28
*	Adaptation au passage de option dans Type	herbelin	2006-05-28
*	encore un exemple ne marchant pas, ni avec omega ni avec romega	letouzey	2006-05-22
*	tests de Romega	letouzey	2006-05-19
*	Centralisation de la détection lettre/symbole par le lexeur dans les plages ...	herbelin	2006-05-10
*	Vieux bug de fin 2004 gardé pour mémoire	herbelin	2006-05-05
*	Ajout bug #1102	herbelin	2006-04-28
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Tests notations	herbelin	2006-04-15
*	- Correction bug calcul mind_consnrealargs, introduit à la révision	herbelin	2006-03-22
*	Ajout test relatif au bug #984	herbelin	2006-03-05
*	Ajout test bug 1089	herbelin	2006-03-02
*	Correction du bug 808: il est maintenant interdit de déclarer une assomption...	coq	2006-03-02
*	Correction bug #842 (rename d'une hyp du contexte)	herbelin	2006-03-01
*	Prise en compte coercions autour des sous-termes filtrés (si non dépendants)	herbelin	2006-01-30
*	Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...	herbelin	2006-01-23
*	Test bug 983	herbelin	2006-01-20
*	Test utf-8	herbelin	2006-01-15
*	Test conflictuel - ajouté pour mémoire	herbelin	2006-01-11
*	Test or-patterns	herbelin	2006-01-11
*	Test bug #1025	herbelin	2005-12-30
*	Mini-test d'extraction	herbelin	2005-12-27
*	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-12-21
*	* empty log message *	mohring	2005-11-03
*	Test reproductibilité du bug #1031	herbelin	2005-11-02
*	Declare Implicit Tactic	herbelin	2005-09-09
*	Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...	herbelin	2005-09-09
*	Test clear final dans intros pattern	herbelin	2005-09-08
*	A wish by Bas Spitters granted: a little more of unification up to	sacerdot	2005-05-19
*	Implemented autorewrite with ... in hyp [using ...].	sacerdot	2005-05-18
*	Ajout Unset Implicit Arguments manquant	herbelin	2005-03-21
*	Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...	herbelin	2005-03-20
*	Ajout test bug #935	herbelin	2005-03-19
*	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin	2005-03-17
*	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin	2005-03-16