coq - The formal proof system

Age	Commit message (Expand)	Author
2002-12-28	Prise en compte notations dans les extensions de motiff	herbelin
2002-12-28	Re-installation nombres dans les motifs sur Z	herbelin
2002-12-24	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin
2002-12-24	code mort	herbelin
2002-12-23	Re-essai de forcer le terme réécrit à apparaître dans le but	herbelin
2002-12-23	Tentative d'interdire les K-abstractions si allow_K est faux et le	herbelin
2002-12-23	Prise en compte application partielle dans dependent	herbelin
2002-12-23	maj	filliatr
2002-12-22	Cas motif universel	herbelin
2002-12-21	Backtrack sur la tentative d'interdire les K-abstractions dans l'unification	herbelin
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-21	Affinement affichage	herbelin
2002-12-21	code mort	herbelin
2002-12-21	Affinement affichage	herbelin
2002-12-21	Plus de notation cablees dans 'annot'	herbelin
2002-12-21	maj	filliatr
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