coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	* empty log message *	barras	2003-03-12
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Petit netoyage dans lib	coq	2002-12-19
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey	2002-12-03
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration de la branche mowgli	herbelin	2002-11-05
*	Lazy manuelles dans le code	coq	2002-10-07
*	Lazy experimentale temporaire...	coq	2002-10-05
*	Suppression automatique du corps des définitions locales opaques dans	herbelin	2002-08-17
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	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-05-29
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	Orthographe	herbelin	2002-01-11
*	reparation du make depend et du .depend	letouzey	2001-12-19
*	Mise en place d'une méthode directe pour indiquer le type des déclarations ...	herbelin	2001-11-19
*	GROS COMMIT:	barras	2001-11-05
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...	herbelin	2001-10-12
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Transparent	barras	2001-09-20
*	Report des modifs de Claudio	herbelin	2001-09-20
*	Parsing	herbelin	2001-08-10
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	application patch Claudio	filliatr	2001-05-11
*	Changement de la structure des points fixes	barras	2001-05-03
*	entetes	filliatr	2001-03-15
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	nouvelle implantation de la reduction	barras	2001-03-01
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin	2001-02-14
*	Absolute URL for DTDs introduced	sacerdot	2001-02-13
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Ajout du Let pour le langage de tactiques	delahaye	2000-12-29
*	Scripts de correction d'uri	herbelin	2000-12-20
*	MAJ	herbelin	2000-12-20
*	Non verbose par défaut	herbelin	2000-12-20
*	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-14
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	type attribute added to PROD (for ForAll vs Pi rendering)	sacerdot	2000-12-07
*	COPYRIGHT file added; some comments changed	sacerdot	2000-12-07
*	Bug identarg au lieu de qualidarg	herbelin	2000-12-06
*	Inner types are now reduced and arrows are created when	sacerdot	2000-12-05
*	LETIN now has a letintarget instead of a target	sacerdot	2000-12-01
*	cictypes.dtd changed	sacerdot	2000-12-01