coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Affinement affichage	herbelin	2002-12-21
*	Plus de notation cablees dans 'annot'	herbelin	2002-12-21
*	maj	filliatr	2002-12-21
*	Prise en compte des coercions dans les 'with' bindings	herbelin	2002-12-20
*	maj	filliatr	2002-12-20
*	Petit netoyage dans lib	coq	2002-12-19
*	suppression de l'archive cvs d'un bout de debug	letouzey	2002-12-19
*	les empty ind et les singletons etaient oublies par add_recursors	letouzey	2002-12-19
*	apres correction du probleme de Global.env, retour du mis_constr_nargs_env	letouzey	2002-12-19
*	bug: Global.env() executé au chargement -> eta-expansion	letouzey	2002-12-19
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	suite du commit precedent	barras	2002-12-19
*	maj	filliatr	2002-12-19
*	- amelioration des messages d'erreur de la condition de garde	barras	2002-12-18
*	stupide inlining des construsteurs	letouzey	2002-12-18
*	Contexte locale non-vide interdit a la fin d'un module ou module type	coq	2002-12-18
*	maj	filliatr	2002-12-18
*	exemple complet de parser	barras	2002-12-17
*	nouveau Subst:	barras	2002-12-17
*	ma bidouille marche pas...	letouzey	2002-12-17
*	Petit netoyage des open's et commentaires	coq	2002-12-16
*	maj	filliatr	2002-12-16
*	MAJ	herbelin	2002-12-15
*	Une entrée spéciale "annot" pour les piquants	herbelin	2002-12-15
*	Ajout syntaxe '>'	herbelin	2002-12-15
*	Traitement spécial pour les types à l'internalisation	herbelin	2002-12-15
*	Ajout "Locate Notation"	herbelin	2002-12-15
*	Prise en compte des scopes traversés dans les notations	herbelin	2002-12-15
*	Meilleure factorisation des entrées NEXT internes	herbelin	2002-12-15
*	Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxe	herbelin	2002-12-15
*	Pas de 0 dans positive	herbelin	2002-12-15
*	Ajout syntaxe '>'	herbelin	2002-12-15
*	Pas d'associativite pour =_D	herbelin	2002-12-15
*	Evaluation paresseuse de l'affichage du debug	herbelin	2002-12-15
*	maj	filliatr	2002-12-14
*	Compensation de suppression betaiota de type_of (suite)	herbelin	2002-12-13
*	debut de parcours des modules	letouzey	2002-12-13
*	une branche de case inutile	letouzey	2002-12-13
*	possibilité de faire Print M avec M module ou modtype au lieu de Print Modul...	letouzey	2002-12-13
*	correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...	letouzey	2002-12-13
*	maj	filliatr	2002-12-13
*	Compensation de suppression betaiota de type_of (suite)	herbelin	2002-12-12
*	* empty log message *	gregoire	2002-12-12
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...	desmettr	2002-12-12
*	maj	filliatr	2002-12-12
*	Essai de hconsing local au declarations	herbelin	2002-12-11
*	Compensation de suppression betaiota de type_of	herbelin	2002-12-11
*	maj	filliatr	2002-12-11
*	Bugs divers	herbelin	2002-12-10