coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing "destruct" test.	herbelin	2011-10-25
*	Use full conversion for checking type of holes in destruct over a	herbelin	2011-10-22
*	Fixing another bug with "_" intro pattern.	herbelin	2011-06-10
*	Made use of "_" in repeated use of intros_patterns work (with	herbelin	2011-06-10
*	Removal of trailing spaces.	serpyc	2009-10-04
*	Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.	herbelin	2009-09-27
*	Delay the choice of eliminator in destruct/induction until we know if	herbelin	2009-09-27
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Add support for dependent "destruct" over terms in dependent types.	herbelin	2009-02-23
*	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin	2008-06-18
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin	2006-12-13
*	Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casse	herbelin	2006-05-31
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	commentaire	herbelin	2004-06-02
*	Protection du destruct pour vérifier que ce n'est pas une anomalie, à défa...	herbelin	2004-05-20
*	Ajout test bug 711	herbelin	2004-05-02