coq - The formal proof system

Age	Commit message (Expand)	Author
2004-03-27	Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; divers	herbelin
2004-03-27	-dead code removed.	sacerdot
2004-03-26	Theory file for file A.B.C.v is put in A/B/C.theory.xml.	sacerdot
2004-03-26	Ajout exportation des 'theory.xml' + divers	herbelin
2004-03-25	ProofTree2Xml is no longer directly used by Xmlcommand.	sacerdot
2004-03-25	Dead code removed.	sacerdot
2004-03-24	Reparation typo de HH dans MAJ de Claudio	herbelin
2004-03-24	MAJ Claudio pour v8	herbelin
2002-12-03	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-05	Intégration de la branche mowgli	herbelin
2001-12-19	reparation du make depend et du .depend	letouzey
2001-11-19	Mise en place d'une méthode directe pour indiquer le type des déclarations ...	herbelin
2001-11-05	GROS COMMIT:	barras
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-12	Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-09-20	Report des modifs de Claudio	herbelin
2001-08-10	Parsing	herbelin
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-11	application patch Claudio	filliatr
2001-05-03	Changement de la structure des points fixes	barras
2001-03-15	entetes	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-02-13	Absolute URL for DTDs introduced	sacerdot
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-20	Non verbose par défaut	herbelin
2000-12-14	Bug sur commit précédent	herbelin
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
2000-12-07	type attribute added to PROD (for ForAll vs Pi rendering)	sacerdot
2000-12-07	COPYRIGHT file added; some comments changed	sacerdot
2000-12-05	Inner types are now reduced and arrows are created when	sacerdot
2000-12-01	LETIN now has a letintarget instead of a target	sacerdot
2000-12-01	cictypes.dtd changed	sacerdot
2000-11-30	Used a force function to force stream evaluation only for aestaetics reasons.	sacerdot
2000-11-30	Identifier order in the inner-types file changed.	sacerdot
2000-11-29	Modifications due to the new As option in AddPath and AddRecPath.	sacerdot
2000-11-29	Now also inner-types are exported.	sacerdot
2000-11-28	Code clean-up due to the new usage of longer names in Coq.	sacerdot
2000-11-28	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin
2000-11-27	Many improvements. Xml contrib retached to the V7.	sacerdot
2000-11-15	Changed the semantics of AddRecPath.	sacerdot
2000-11-09	Renommage canonique SectionLocalDecl -> SectionLocalAssum	herbelin
2000-11-08	nouveau load path	filliatr
2000-11-08	First version with out_variable used. Exports all the standard library	sacerdot