aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/destruct.v
AgeCommit message (Expand)Author
2011-10-25Fixing "destruct" test.herbelin
2011-10-22Use full conversion for checking type of holes in destruct over aherbelin
2011-06-10Fixing another bug with "_" intro pattern.herbelin
2011-06-10Made use of "_" in repeated use of intros_patterns work (withherbelin
2009-10-04Removal of trailing spaces.serpyc
2009-09-27Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.herbelin
2009-09-27Delay the choice of eliminator in destruct/induction until we know ifherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-02-23Add support for dependent "destruct" over terms in dependent types.herbelin
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2006-12-13Dépliage du terme d'induction avant suppression quand celui-ci est unherbelin
2006-05-31Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseherbelin
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2004-06-02commentaireherbelin
2004-05-20Protection du destruct pour vérifier que ce n'est pas une anomalie, à défa...herbelin
2004-05-02Ajout test bug 711herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-10 05:11:09 +0000