coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-21	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin
2006-10-17	Clarification des contraintes sur le contexte de paramètres des	herbelin
2006-10-13	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin
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-10-06	suite commit 9222 : rétablissement des tests autre que complexité	herbelin
2006-10-06	Ajout d'un répertoire de test de la complexité	herbelin
2006-10-05	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin
2006-10-02	nouveau ring/field	barras
2006-10-01	Une passe sur l'injection et la discrimination...	herbelin
2006-09-25	Corrections mineures	notin
2006-09-23	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin
2006-09-23	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin
2006-09-23	Wish #1187 granted (support for canonical structures that are records	herbelin
2006-09-23	Correction bug #1229 (toplevel "unresolved evar" fled through	herbelin
2006-09-23	- Correction filtrage des notations impliquant un "match" : la présence	herbelin
2006-09-22	Test Tactic Notation	herbelin
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-09-14	Correction du bug #1181	jforest
2006-09-12	Ajout unification pattern dans l'algorithme d'unification des	herbelin
2006-09-01	Extension et réorganisation de l'interprétation des (co-)points fixes	herbelin
2006-08-28	Diverses modifications autour de l'unification modulo conversion:	herbelin
2006-08-22	+ 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-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	Stricte positivité en présence de types inductifs imbriqués avec paramètr...	herbelin
2006-06-23	modifs de test-suite suite au passage des graphes de Function dans Type	jforest
2006-06-22	Deux vérifications que le polymorphisme de sorte des inductifs ne fonctionne...	herbelin
2006-06-09	Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...	herbelin
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 sig2 dans Type	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-13	Correction trou de typage des éliminations d'inductifs introduit dans commit...	herbelin
2006-05-10	Conformité nouveaux principes: Declare Module non utilisable pour définir u...	herbelin
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-24	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin