coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Gestion espaces dans notation _ = _ :> _	herbelin	2007-06-05
*	Amélioration de la complexité de auto (l'utilisation des types dans	herbelin	2007-06-05
*	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-30
*	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-29
*	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-28
*	As suggested by Pierre Casteran, fold for FSets/FMaps now takes a	letouzey	2007-05-27
*	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-25
*	fixed (PR#1483)	corbinea	2007-05-24
*	Unification suite: petits affinements pour préserver la compatibilité	herbelin	2007-05-24
*	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-23
*	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-22
*	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-21
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Backtrack sur l'effacement dans le contexte de but des lieurs	herbelin	2007-05-19
*	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-18
*	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-17
*	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	2007-05-16
*	Correction du pretty-printing des big-int (la sous-fonction get_height	aspiwack	2007-05-15
*	pos_mod fixed	thery	2007-05-15
*	Correction de sqrt312 (racine carree d'un nombre represente comme un	aspiwack	2007-05-15
*	corrections bug dans l'implem de int31	bgregoir	2007-05-15
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Made some places in the reference manual clearer. Corrected	emakarov	2007-05-11
*	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin	2007-05-10
*	Correction du bug #1509	notin	2007-05-07
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06