coq - The formal proof system

Age	Commit message (Expand)	Author
2007-06-09	Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...	msozeau
2007-06-08	some more properties of fold and elements in FSetProperties	letouzey
2007-06-08	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov
2007-06-07	Extension of NArith: Nminus, Nmin, etc	letouzey
2007-06-07	* For uniformity, FSetAVL uses Implicit Arguments (a bit)	letouzey
2007-06-07	Ajout doc clear sans argument	herbelin
2007-06-07	Unification des types + clause filtrage manquante + uniformisation locale	herbelin
2007-06-06	Toujours l'unification de apply : nouveau raffinement pour ne tester	herbelin
2007-06-06	tail0	thery
2007-06-05	Gestion espaces dans notation _ = _ :> _	herbelin
2007-06-05	Amélioration de la complexité de auto (l'utilisation des types dans	herbelin
2007-05-30	Corrections dans le Print Assumption. Les definitions locales ("Let")	aspiwack
2007-05-30	Memory optimisation for modules and constrs substitutions.	soubiran
2007-05-30	mul_norm for Q fixed	thery
2007-05-29	Corrected the treatment of negative numbers for the bigZ parser. And	aspiwack
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-28	comparison functions should be Defined not Qed	letouzey
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-28	Retour à un message d'erreur d'apply qui montre un échec sans sans réduction	herbelin
2007-05-28	Réaffichage des Structure/Record sous la forme Record	herbelin
2007-05-27	As suggested by Pierre Casteran, fold for FSets/FMaps now takes a	letouzey
2007-05-25	fix for bug #1347 (no more Scope pollution by FSets)	letouzey
2007-05-25	Modification of VernacScheme to handle a new scheme: Equality (equality in	vsiles
2007-05-25	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9859 85f007b7-540e-04...	soubiran
2007-05-25	Correction of (PR#1576).	soubiran
2007-05-24	fixed (PR#1483)	corbinea
2007-05-24	Unification suite: petits affinements pour préserver la compatibilité	herbelin
2007-05-23	Tentative d'insertion de coercions avant unification si le type de la	herbelin
2007-05-23	A fix for bug #1397:	letouzey
2007-05-23	Suite restructuration unification et division des problèmes	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-22	Comparaison JMeq/eq_dep	herbelin
2007-05-22	Par compatibilité, les implicites terminaux sont maximaux aussi quand	herbelin
2007-05-21	Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le	herbelin
2007-05-21	Added Z and Q implementations with int31.	aspiwack
2007-05-21	add_mul_pos uses int31 only	thery
2007-05-21	MAJ	herbelin
2007-05-21	Protection d'un warning par if_verbose	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-19	Backtrack sur l'effacement dans le contexte de but des lieurs	herbelin
2007-05-18	Interprétation des listes de VarArgType dans les notations faisant	herbelin
2007-05-18	Wish #1582 (3eme)	herbelin
2007-05-18	Quelques essais autour du wish implicite au rapport de bug #1582 (2eme)	herbelin
2007-05-18	Quelques essais autour du wish implicite au rapport de bug #1582	herbelin
2007-05-17	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest
2007-05-17	Nettoyage et standardisation des messages d'erreurs.	herbelin
2007-05-17	Correction des bugs #1537 (anomalie sur signature incomplète) et #1536	herbelin
2007-05-17	Fixed bug #1540 (typo on name .coqide-gtk2rc)	herbelin
2007-05-16	Correction bug calcul des implicites en présence d'evars dans les types	herbelin
2007-05-16	- MAJ entêtes des fichiers produits par coq_makefile	herbelin