coq - The formal proof system

Age	Commit message (Expand)	Author
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
2007-05-15	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-11	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-10	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin
2007-05-07	Correction du bug #1509	notin
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-30	Modification syntaxe de Test	herbelin
2007-04-29	Orthographe en passant	herbelin
2007-04-29	Quelques exemples sur l'asymétrie de la conversion	herbelin
2007-04-29	Plus d'option -v8 dans coqmktop	herbelin
2007-04-29	Multiples changements autour des implicites :	herbelin
2007-04-29	Suite commit 9810	herbelin
2007-04-29	Ajout possibilité d'options à trois mots.	herbelin
2007-04-29	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin
2007-04-28	Correction bug #1519	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2007-04-28	Déplacement des opérations sur bool dans l'état initial	herbelin
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin