coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Renommage de RealsB en Rbase	desmettr	2003-01-16
*	Renommage de Rbase.v en RIneq.v	desmettr	2003-01-16
*	maj	filliatr	2003-01-16
*	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin	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-15
*	patch configure (V Aymeric)	filliatr	2003-01-13
*	maj	filliatr	2003-01-10
*	Export M + Module M <: SIG	coq	2003-01-09
*	correction de bug de Subst: ne faisait rien lorsque l'hypothese	barras	2003-01-09
*	maj	filliatr	2003-01-08
*	Retour printer ast pour V7.4	herbelin	2003-01-07
*	maj	filliatr	2003-01-07
*	SearchAbout	filliatr	2003-01-06
*	bit vectors	filliatr	2003-01-06
*	Amélioration règles d'affichage	herbelin	2002-12-31
*	Commentaires; optimisation	herbelin	2002-12-30
*	Amélioration choix des noms dans abstract_list_all	herbelin	2002-12-30
*	Prise en compte notations dans les extensions de motiff	herbelin	2002-12-28
*	Re-installation nombres dans les motifs sur Z	herbelin	2002-12-28
*	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin	2002-12-24
*	code mort	herbelin	2002-12-24
*	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-23
*	Cas motif universel	herbelin	2002-12-22
*	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-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