coq - The formal proof system

Age	Commit message (Expand)	Author
2007-02-21	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin
2007-02-21	Removed some useless code in mod_typing that was redundant with safe_typing.	soubiran
2007-02-21	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran
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-28	Pas de solution à court terme pour ce problème de complexité	herbelin
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-19	Prise en compte des univers algébriques dans les types inférés dans	herbelin
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
2007-01-12	Suite au mail de Lionel a propos du Makefile:	letouzey
2006-12-28	Correction petits bugs du check de la test-suite	herbelin
2006-12-22	remplacement d'un test d'egalite par un test de convertibilite dans injection...	jforest
2006-12-13	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin
2006-12-13	test condition de garde	barras
2006-12-13	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin
2006-12-12	Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...	herbelin
2006-12-12	MAJ	herbelin
2006-12-12	Test bug #932	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	Corrige un bug de calcul du temps effectif cquand la dernière décimale est 0	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-11-03	bug test complexité	herbelin
2006-11-01	Ajout test setoid_rewrite (cf bug #1176); anglicisation	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-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-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-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