coq - The formal proof system

Age	Commit message (Expand)	Author
2008-02-08	Add more information to IllFormedRecBody exceptions, to show the exact	msozeau
2008-02-01	Beaoucoup de changements dans la representation interne des modules.	soubiran
2008-01-31	Finish let\| implementation and document it	msozeau
2008-01-18	bug in accessing n-th abstraction	barras
2008-01-05	Fixed bug 1761 (unexpected anomaly when constructor type has invalid	herbelin
2007-12-31	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau
2007-12-18	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-11-09	Nettoyage de Print Assumptions :	aspiwack
2007-11-07	bug in infos_and_sort: type of constructor was not reduced enough	barras
2007-10-30	bug in safe_typing: univ constraints generated by section variables were not ...	barras
2007-10-04	Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)	herbelin
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2007-09-15	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey
2007-08-27	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin
2007-07-12	normalisation (by closure) was not performed under fixpoints	barras
2007-06-26	kill an ugly warning about a non-exhaustive pattern	letouzey
2007-06-21	Correction de plusieurs bugs de l'export XML (utilisation d'un type de	herbelin
2007-06-20	ajout de head0 et tail0 en natif	bgregoir
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-25	Correction of (PR#1576).	soubiran
2007-05-23	Suite restructuration unification et division des problèmes	herbelin
2007-05-17	Nettoyage et standardisation des messages d'erreurs.	herbelin
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-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-04-05	Correction partielle du bug #1388 (augmentation de la taille des code accepte...	jforest
2007-03-27	Modification de la vm:	notin
2007-03-15	Suppression argument pattern_source du case_info (code jamais utilisé)	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-09	Suppresion de la catégorie des inductifs singletons larges dont	herbelin
2007-02-01	Suppression de code mort	notin
2007-01-30	suite du commit 9557	soubiran
2007-01-30	Petite correction sur un message d'erreur renvoyé au sous typage.	soubiran
2007-01-24	modifications des messages d'erreurs renvoyés lors de la comparaison	soubiran
2007-01-22	Correction du bug #1315:	notin
2007-01-19	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-17	Correction bug #1302	herbelin
2006-12-12	Correction du bug #1273 (problème avec les paramètres non récursivement un...	notin
2006-12-12	cosmetique	barras
2006-12-11	Changement dans le kernel :	bgregoir
2006-12-08	bug condition de garde	barras
2006-10-30	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin
2006-10-30	dependences	barras
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-27	Ajout fold_rel_declaration et fold_named_declaration	herbelin