aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/destruct.v
Commit message (Expand)AuthorAge
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.Gravatar herbelin2009-09-27
* Delay the choice of eliminator in destruct/induction until we know ifGravatar herbelin2009-09-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Dépliage du terme d'induction avant suppression quand celui-ci est unGravatar herbelin2006-12-13
* Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseGravatar herbelin2006-05-31
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* commentaireGravatar herbelin2004-06-02
* Protection du destruct pour vérifier que ce n'est pas une anomalie, à défa...Gravatar herbelin2004-05-20
* Ajout test bug 711Gravatar herbelin2004-05-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 12:58:59 +0000