coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suite au mail de Lionel a propos du Makefile:	letouzey	2007-01-12
*	Correction petits bugs du check de la test-suite	herbelin	2006-12-28
*	remplacement d'un test d'egalite par un test de convertibilite dans injection...	jforest	2006-12-22
*	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin	2006-12-13
*	test condition de garde	barras	2006-12-13
*	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin	2006-12-13
*	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
*	Raffinement de l'unification de "apply": mémorisation de certains	herbelin	2006-11-19
*	Corrige un bug de calcul du temps effectif cquand la dernière décimale est 0	herbelin	2006-11-13
*	Correction typo	herbelin	2006-11-13
*	Ajout de dépliage de l'énoncé, si besoin est, dans apply in	herbelin	2006-11-10
*	Correction d'un bug refine	herbelin	2006-11-10
*	bug test complexité	herbelin	2006-11-03
*	Ajout test setoid_rewrite (cf bug #1176); anglicisation	herbelin	2006-11-01
*	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin	2006-10-30
*	missing Require LegacyRfield	barras	2006-10-30
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Check that sort-polymorphic inductive types is not too lax	herbelin	2006-10-27
*	Cette dérivation de paradoxe passait en V8.1beta	herbelin	2006-10-27
*	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin	2006-10-25
*	Test apply in	herbelin	2006-10-24
*	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin	2006-10-21
*	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin	2006-10-21
*	Clarification des contraintes sur le contexte de paramètres des	herbelin	2006-10-17
*	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin	2006-10-13
*	Correction test-suite suite à r9186	notin	2006-10-13
*	Exemple avec liaison des variables de filtrage du match	herbelin	2006-10-09
*	Notations:	herbelin	2006-10-09
*	suite commit 9222 : rétablissement des tests autre que complexité	herbelin	2006-10-06
*	Ajout d'un répertoire de test de la complexité	herbelin	2006-10-06
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
*	nouveau ring/field	barras	2006-10-02
*	Une passe sur l'injection et la discrimination...	herbelin	2006-10-01
*	Corrections mineures	notin	2006-09-25
*	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin	2006-09-23
*	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin	2006-09-23
*	Wish #1187 granted (support for canonical structures that are records	herbelin	2006-09-23
*	Correction bug #1229 (toplevel "unresolved evar" fled through	herbelin	2006-09-23
*	- Correction filtrage des notations impliquant un "match" : la présence	herbelin	2006-09-23
*	Test Tactic Notation	herbelin	2006-09-22
*	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin	2006-09-15
*	Correction du bug #1181	jforest	2006-09-14
*	Ajout unification pattern dans l'algorithme d'unification des	herbelin	2006-09-12
*	Extension et réorganisation de l'interprétation des (co-)points fixes	herbelin	2006-09-01
*	Diverses modifications autour de l'unification modulo conversion:	herbelin	2006-08-28
*	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest	2006-08-22
*	remove an orphan comment (attached to a piece of code that was removed).	bertot	2006-08-22