coq - The formal proof system

Age	Commit message (Expand)	Author
2004-03-24	MAJ Claudio pour v8	herbelin
2004-03-24	Reparation typo de HH dans MAJ de Claudio	herbelin
2004-03-24	MAJ Claudio pour v8	herbelin
2004-03-24	Utilisation du printer approprie a la version de syntaxe	herbelin
2004-03-24	Nettoyage	herbelin
2004-03-24	Effacement tardif de ce fichier qui a ete transforme le 5 nov 2002 en une ver...	herbelin
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-12	* empty log message *	barras
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin
2002-12-19	Petit netoyage dans lib	coq
2002-12-19	simplification de solve_subgoal: n'utilise plus frontier	barras
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
2002-10-07	Lazy manuelles dans le code	coq
2002-10-05	Lazy experimentale temporaire...	coq
2002-08-17	Suppression automatique du corps des définitions locales opaques dans	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-05-29	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin
2002-05-29	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2002-01-11	Orthographe	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	Scripts de correction d'uri	herbelin
2000-12-20	MAJ	herbelin
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-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr