coq - The formal proof system

Age	Commit message (Expand)	Author
2006-12-28	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin
2006-12-28	Correction petits bugs du check de la test-suite	herbelin
2006-12-28	Remplacement de la définition de Pind et Prec par une définition	herbelin
2006-12-28	Cleaning backtracking code, optimized "Backtrack n x y" when n is	courtieu
2006-12-26	Report correction bug #1289 dans trunk (r9435 pour branche v8.1)	herbelin
2006-12-23	Doc for Combined Scheme.	msozeau
2006-12-23	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau
2006-12-22	Default tactic for solving goals.	msozeau
2006-12-22	remplacement d'un test d'egalite par un test de convertibilite dans injection...	jforest
2006-12-21	typo malencontreuse	filliatr
2006-12-19	Adaptation à Subversion 1.4	notin
2006-12-17	reparation bug 1239	letouzey
2006-12-15	Changement dans ring et field, beaucoup de correction d'erreurs,	bgregoir
2006-12-15	contrib/dp: tactique ergo (voir ergo.lri.fr)	filliatr
2006-12-14	Confusion sur le paramètre à donner à concrete_name lors du commit 9450	herbelin
2006-12-14	Reimplemented equality generation for pattern matching at typing time. First ...	msozeau
2006-12-13	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin
2006-12-13	test condition de garde	barras
2006-12-13	svn:ignore	herbelin
2006-12-13	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin
2006-12-12	Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...	notin
2006-12-12	Correction du bug #1273 (problème avec les paramètres non récursivement un...	notin
2006-12-12	Subtac: work on cases.	msozeau
2006-12-12	nouvelle indentation des scripts	barras
2006-12-12	cosmetique	barras
2006-12-12	Variable print_instances pour dÃ©boguer les instances d'evar	herbelin
2006-12-12	Dépendence inutile	herbelin
2006-12-12	AllÃègement de syntxe suite à l'introduction de l'unif pattern	herbelin
2006-12-12	Bug nommage Zgt_trans_succ	herbelin
2006-12-12	Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...	herbelin
2006-12-12	MAJ	herbelin
2006-12-12	Test bug #932	herbelin
2006-12-12	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin
2006-12-11	correction Open Local Scope (Ring)	bgregoir
2006-12-11	Changement dans le kernel :	bgregoir
2006-12-09	Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)	herbelin
2006-12-09	Évitement des noms de constructeurs dans les motifs de filtrage de "match"	herbelin
2006-12-09	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 85f007b7-540e-04...	filliatr
2006-12-08	bug condition de garde	barras
2006-12-08	dp	filliatr
2006-12-08	contrib/dp	filliatr
2006-12-08	Pas d'escamotage des noms rÃ©servÃ©s si Set Printing All actibvÃ©	herbelin
2006-12-08	Suite ajout option -output-context	herbelin
2006-12-08	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 85f007b7-540e-04...	filliatr
2006-12-08	Ajout d'une option -output-context qui affiche le contexte en CCI pur à la	herbelin
2006-12-08	Correction typo règle réduction du fix chapitre CCI	herbelin
2006-12-08	Subtac bug fix, add list take example.	msozeau
2006-12-03	MAJ	herbelin
2006-12-03	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin
2006-12-01	add a comment about Show Existentials and a question about case_eq	jnarboux