aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/destruct.v
Commit message (Expand)AuthorAge
* Take benefit of improved name preservation of evars in e2fa65fcc.Gravatar Hugo Herbelin2014-12-04
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
* Preserving the good effect of 014e5ac92a on not leaving dangling localGravatar Hugo Herbelin2014-11-14
* Removing yet another source of remaining local definitions.Gravatar Hugo Herbelin2014-11-13
* Restoring clear_flag (thanks a lot to jonikelee to notice it).Gravatar Hugo Herbelin2014-11-06
* Optimizing when to clear generalized hypotheses in destruct.Gravatar Hugo Herbelin2014-11-06
* Removing "destruct" test not yet working.Gravatar Hugo Herbelin2014-11-06
* Subtle swap of lines to preserve VarInstance src field before checkingGravatar Hugo Herbelin2014-11-03
* Fix to 844431761 on improving elimination with indices, getting rid ofGravatar Hugo Herbelin2014-11-03
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Some reorganization of the code for destruct/induction:Gravatar Hugo Herbelin2014-11-02
* Fixing file destruct.v.Gravatar Hugo Herbelin2014-11-02
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* Listing a few examples of destruct showing unsatisfactory behaviors.Gravatar Hugo Herbelin2014-10-31
* Avoid "destruct H" to apply on H itself when H is a section variable.Gravatar Hugo Herbelin2014-10-31
* Making destruct on idents with maximal implicit arguments working, byGravatar Hugo Herbelin2014-10-27
* Ensuring compatibility when an hypothesis used for destruct isGravatar Hugo Herbelin2014-10-27
* Fixing clash in test destruct.v.Gravatar Hugo Herbelin2014-10-27
* Fixing destruct/induction with a using clause on a non-inductive type,Gravatar Hugo Herbelin2014-10-26
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Fixing an unnatural selection of subterms larger than expected in theGravatar Hugo Herbelin2014-08-28
* Fixing unification of subterms identified by patterns.Gravatar Hugo Herbelin2014-08-18
* Fixing "destruct" test.Gravatar herbelin2011-10-25
* Use full conversion for checking type of holes in destruct over aGravatar herbelin2011-10-22
* Fixing another bug with "_" intro pattern.Gravatar herbelin2011-06-10
* Made use of "_" in repeated use of intros_patterns work (withGravatar herbelin2011-06-10
* 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-10-30 02:05:43 +0000