coq - The formal proof system

Age	Commit message (Expand)	Author
2002-12-20	Prise en compte des coercions dans les 'with' bindings	herbelin
2002-12-20	maj	filliatr
2002-12-19	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-18	- 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-17	exemple complet de parser	barras
2002-12-17	nouveau Subst:	barras
2002-12-17	ma bidouille marche pas...	letouzey
2002-12-16	Petit netoyage des open's et commentaires	coq
2002-12-16	maj	filliatr
2002-12-15	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-14	maj	filliatr
2002-12-13	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-12	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-11	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-10	Bugs divers	herbelin
2002-12-10	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin
2002-12-10	Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)	herbelin
2002-12-10	Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse la	herbelin