coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	changement des _sym par _comm dans setoid_ring	bgregoir	2006-10-27
*	Le caractère ² fait planter make doc	notin	2006-10-27
*	Check that sort-polymorphic inductive types is not too lax	herbelin	2006-10-27
*	Fixes on functional graphs merging: removed debug printing.	courtieu	2006-10-27
*	Fixes on functional graphs merging: names of constructors.	courtieu	2006-10-27
*	Cette dérivation de paradoxe passait en V8.1beta	herbelin	2006-10-27
*	Restriction au implémenteurs	herbelin	2006-10-27
*	Ajout ListTactics	herbelin	2006-10-27
*	Ajout ListTactics	herbelin	2006-10-27
*	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin	2006-10-26
*	Affichage d'un message d'erreur losque qu'une relation n'a pas été déclar�...	notin	2006-10-26
*	Noms de compatibilité déplacés en bloc à la fin du fichier	herbelin	2006-10-26
*	Some fixes in experimental merging of two functional graphs.	courtieu	2006-10-26
*	added doc for declarative language	corbinea	2006-10-26
*	Experimental merging of two functional graphs.	courtieu	2006-10-26
*	Facilities to automatically solve obligations	msozeau	2006-10-26
*	MAJ crédits, fresh; documentation apply in	herbelin	2006-10-26
*	MAJ	herbelin	2006-10-26
*	Petit bug apply in	herbelin	2006-10-26
*	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin	2006-10-25
*	Suite commit 9277	herbelin	2006-10-25
*	oups, ne chargeait pas les bons fichiers	letouzey	2006-10-25
*	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin	2006-10-25
*	coqdep -slash	barras	2006-10-25
*	Ménage	notin	2006-10-25
*	oops	barras	2006-10-25
*	conflit de nom (Field_theory) modulo la casse	barras	2006-10-25
*	Extension de fresh (suite)	herbelin	2006-10-24
*	Changement de la valeur par défaut de with_geoproof (stabilité coqide)	notin	2006-10-24
*	Test apply in	herbelin	2006-10-24
*	Insère une coercion vers Sortclass dans 'contradiction' si nécessaire	herbelin	2006-10-24
*	Ajout de la tactique 'remember'	herbelin	2006-10-24
*	Extension de la primitive ltac fresh pour qu'elle accepte une liste de	herbelin	2006-10-24
*	Ajout de la tactique "apply in".	herbelin	2006-10-24
*	Hack peu élégant pour permettre de parser des listes avec séparateurs dans	herbelin	2006-10-24
*	Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén...	herbelin	2006-10-24
*	fixed same_file (#1141)	barras	2006-10-23
*	fixed non-bug #1213	barras	2006-10-23
*	bug #1194: normalisation evars a la sortie de focus	barras	2006-10-23
*	Fixed "Show intros" which did not look at hypothesis.	courtieu	2006-10-23
*	Add a flush after backtracking x y z and before printing subgoals.	courtieu	2006-10-23
*	Add a flush for a warning.	courtieu	2006-10-23
*	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin	2006-10-21
*	Pas d'@ dans les identificateurs (pour F4 and co)	herbelin	2006-10-21
*	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin	2006-10-21
*	MAJ	herbelin	2006-10-20
*	Correction du bug #1255 (réécriture setoid sous un produit)	notin	2006-10-20
*	Correction de la localisation des erreurs en interactif (numéro de	herbelin	2006-10-20
*	Starting to add a function schemes merging command (not finished, not	courtieu	2006-10-20
*	Correction sym -> comm	herbelin	2006-10-19