coq - The formal proof system

Age	Commit message (Expand)	Author
2003-01-15	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin
2003-01-15	Bug en présence de let-in	herbelin
2003-01-15	Nouvelle interprétation des nombres réels	desmettr
2003-01-15	Bug en présence de let-in	herbelin
2003-01-15	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin
2003-01-13	patch configure (V Aymeric)	filliatr
2003-01-10	maj	filliatr
2003-01-09	Export M + Module M <: SIG	coq
2003-01-09	correction de bug de Subst: ne faisait rien lorsque l'hypothese	barras
2003-01-08	maj	filliatr
2003-01-07	Retour printer ast pour V7.4	herbelin
2003-01-07	maj	filliatr
2003-01-06	SearchAbout	filliatr
2003-01-06	bit vectors	filliatr
2002-12-31	Amélioration règles d'affichage	herbelin
2002-12-30	Commentaires; optimisation	herbelin
2002-12-30	Amélioration choix des noms dans abstract_list_all	herbelin
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