coq - The formal proof system

Age	Commit message (Expand)	Author
2007-07-09	Improvements / Bug fixes for ROmega	letouzey
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-24	Unification suite: petits affinements pour préserver la compatibilité	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-18	Wish #1582 (3eme)	herbelin
2007-05-16	Correction bug calcul des implicites en présence d'evars dans les types	herbelin
2007-04-30	Modification syntaxe de Test	herbelin
2007-04-29	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin
2007-04-13	Correction bug #1477 sur ordre des variables partagées par les or-patterns.	herbelin
2007-04-13	Test non régression bug #1491	herbelin
2007-03-15	Test de non-régression pour commit 9673	herbelin
2007-02-21	Correction typo liée au commit 8779 (levait une anomalie)	herbelin
2007-02-21	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin
2007-02-15	Réparation absence d'interprétation des liaisons vers listes	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-01	Report de la révision 9577 dans le trunk	notin
2007-01-25	Redondance erronée dans les tests	herbelin
2007-01-22	Correction d'un bug d'unification-pattern dans l'algo d'unification	herbelin
2007-01-22	Correction pour le rapport de bug #1325 par rétablissement du	herbelin
2007-01-12	Suite au mail de Lionel a propos du Makefile:	letouzey
2006-12-13	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin
2006-12-13	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin
2006-12-12	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin
2006-11-19	Raffinement de l'unification de "apply": mémorisation de certains	herbelin
2006-11-13	Correction typo	herbelin
2006-11-10	Ajout de dépliage de l'énoncé, si besoin est, dans apply in	herbelin
2006-11-10	Correction d'un bug refine	herbelin
2006-10-30	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin
2006-10-30	missing Require LegacyRfield	barras
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-25	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin
2006-10-24	Test apply in	herbelin
2006-10-21	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin
2006-10-21	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin
2006-10-13	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin
2006-10-02	nouveau ring/field	barras
2006-10-01	Une passe sur l'injection et la discrimination...	herbelin
2006-09-23	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin
2006-09-23	Wish #1187 granted (support for canonical structures that are records	herbelin
2006-09-22	Test Tactic Notation	herbelin
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
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