coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	bug in infos_and_sort: type of constructor was not reduced enough	barras	2007-11-07
*	bug in safe_typing: univ constraints generated by section variables were not ...	barras	2007-10-30
*	Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)	herbelin	2007-10-04
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	normalisation (by closure) was not performed under fixpoints	barras	2007-07-12
*	kill an ugly warning about a non-exhaustive pattern	letouzey	2007-06-26
*	Correction de plusieurs bugs de l'export XML (utilisation d'un type de	herbelin	2007-06-21
*	ajout de head0 et tail0 en natif	bgregoir	2007-06-20
*	Corrections dans le Print Assumption. Les definitions locales ("Let")	aspiwack	2007-05-30
*	Memory optimisation for modules and constrs substitutions.	soubiran	2007-05-30
*	Correction of (PR#1576).	soubiran	2007-05-25
*	Suite restructuration unification et division des problèmes	herbelin	2007-05-23
*	Nettoyage et standardisation des messages d'erreurs.	herbelin	2007-05-17
*	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
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	Correction partielle du bug #1388 (augmentation de la taille des code accepte...	jforest	2007-04-05
*	Modification de la vm:	notin	2007-03-27
*	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin	2007-03-15
*	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-21
*	Suppresion de la catégorie des inductifs singletons larges dont	herbelin	2007-02-09
*	Suppression de code mort	notin	2007-02-01
*	suite du commit 9557	soubiran	2007-01-30
*	Petite correction sur un message d'erreur renvoyé au sous typage.	soubiran	2007-01-30
*	modifications des messages d'erreurs renvoyés lors de la comparaison	soubiran	2007-01-24
*	Correction du bug #1315:	notin	2007-01-22
*	Prise en compte des univers algébriques dans les types inférés dans	herbelin	2007-01-19
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	Correction bug #1302	herbelin	2007-01-17
*	Correction du bug #1273 (problème avec les paramètres non récursivement un...	notin	2006-12-12
*	cosmetique	barras	2006-12-12
*	Changement dans le kernel :	bgregoir	2006-12-11
*	bug condition de garde	barras	2006-12-08
*	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin	2006-10-30
*	dependences	barras	2006-10-30
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	Ajout fold_rel_declaration et fold_named_declaration	herbelin	2006-10-27
*	Correction de 2 bugs critiques du polymorphisme d'univers	herbelin	2006-10-27
*	changement des _sym par _comm dans setoid_ring	bgregoir	2006-10-27
*	Clarification des contraintes sur le contexte de paramètres des	herbelin	2006-10-17
*	Protection raise en début de séquence (en attendant que le code caché trou...	herbelin	2006-10-12
*	Déplacement de on_judgment_type de Typeops vers Termops	herbelin	2006-10-06
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
*	Changement de comportement du [rewrite ... in H]: Coq échoue si H	notin	2006-10-03
*	Correction du bug #1181	jforest	2006-09-14
*	Indentation + typo	notin	2006-09-01