coq - The formal proof system

Age	Commit message (Expand)	Author
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-08-31	V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclass	herbelin
2003-06-11	Pb quand une meme classe est definie dans 2 fichiers	herbelin
2003-06-08	Tables logarithmiques pour les coercions + nettoyage	herbelin
2003-03-12	* empty log message *	barras
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-01-18	Le chargement des coercions est nécessaire même si le module n'est pas ouvert	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-12-11	Mise en place de coercion dans les motifs	herbelin
2001-11-20	Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant	herbelin
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