coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-28
*	Report correction bug #1289 dans trunk (r9435 pour branche v8.1)	herbelin	2006-12-26
*	Doc for Combined Scheme.	msozeau	2006-12-23
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	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-22
*	typo malencontreuse	filliatr	2006-12-21
*	Adaptation à Subversion 1.4	notin	2006-12-19
*	reparation bug 1239	letouzey	2006-12-17
*	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-15
*	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-14
*	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-13
*	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-12
*	correction Open Local Scope (Ring)	bgregoir	2006-12-11
*	Changement dans le kernel :	bgregoir	2006-12-11
*	É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-09
*	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-08
*	MAJ	herbelin	2006-12-03
*	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin	2006-12-03
*	add a comment about Show Existentials and a question about case_eq	jnarboux	2006-12-01