coq - The formal proof system

Age	Commit message (Expand)	Author
2001-11-09	Nettoyage coercions et classes	herbelin
2001-11-05	GROS COMMIT:	barras
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-08-10	Parsing	herbelin
2001-07-06	Les tables de coercions ne doivent pas survivre aux sections	herbelin
2001-07-05	Débogage discharge des coercions; nettoyage	herbelin
2001-07-04	message Ambiguous paths seulement si verbose	filliatr
2001-03-15	entetes	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-02-06	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin
2001-02-05	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin
2000-12-25	Un nom long pour les variables de section qui font classe ou coercion; réorg...	herbelin
2000-11-26	Remplacement de certains sp_of_id par des locate	herbelin
2000-11-24	certains effets disparaissent a la sortie des sections, d'autres non (selon S...	filliatr
2000-11-20	Utilisation de global_reference dans rawconstr	herbelin
2000-11-15	methode export	filliatr
2000-11-10	Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...	herbelin
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-01	Renommage AppL en App	herbelin
2000-09-12	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-08-08	reparation bug des coercions (cas ou on importe une coercion faisant	barras
2000-01-07	Déplacement non-affichage des coercions dans termast	herbelin
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-05	changement type add_anonymous_leaf	filliatr
1999-12-02	Modifs suite à intégration de class.ml	herbelin
1999-12-02	affichage classes et coercions	filliatr
1999-12-01	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin
1999-11-29	portage Astterm (partiellement)	filliatr
1999-11-26	module Classops; ajout de fonctions dans Declare en consequence	filliatr
1999-11-25	Des progres dans l'integration	herbelin
1999-11-24	Versions initiales	herbelin