aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2014-11-25Tweak some test cases.Xavier Clerc
2014-11-25Adapting to current semantics of "simpl non-evaluable-cst"Hugo Herbelin
2014-11-25Experimenting using unification when matching evar/meta free subtermsHugo Herbelin
2014-11-24Adding test for bug #3248.Pierre-Marie Pédrot
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-11-22Test for closed #2713 and #2876.Hugo Herbelin
2014-11-22Add test-suite file for dependent rewriting example by Vadim Zaliva andMatthieu Sozeau
2014-11-21Adding test for bug #3326.Pierre-Marie Pédrot
2014-11-21Adding test for bug #3424.Pierre-Marie Pédrot
2014-11-21Cleaning up closed bugs in test-suite.Pierre-Marie Pédrot
2014-11-21Test for bug #3788.Pierre-Marie Pédrot
2014-11-21Add test-suite file for bug #3804.Matthieu Sozeau
2014-11-20Adding test for bug #3684.Pierre-Marie Pédrot
2014-11-18Fixing a little bug with nested but convertible occurrences in "destruct at".Hugo Herbelin
2014-11-18Fixing detection of occurrences in the presence of nested subterms forHugo Herbelin
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-14Use return code to classify anomalies as active open bugs.Xavier Clerc
2014-11-14Add missing "Fail" to test case for bug #2814.Xavier Clerc
2014-11-14Reproduction cases for the test suite.Xavier Clerc
2014-11-14Preserving the good effect of 014e5ac92a on not leaving dangling localHugo Herbelin
2014-11-13Removing yet another source of remaining local definitions.Hugo Herbelin
2014-11-11Adapting output tests to current naming of evars, even if unclearHugo Herbelin
2014-11-09Adding test for bug 3792.Pierre-Marie Pédrot
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-11-08Compatibility with 8.4 in the heuristic used to build the inductionHugo Herbelin
2014-11-08Test #3655 was failing due to an anomaly. Now it rather has to failHugo Herbelin
2014-11-08Test fixed by PMP's commits from Oct 21.Hugo Herbelin
2014-11-07Test for #3675 on primitive projections.Hugo Herbelin
2014-11-07Fixing #3562 ("as" in "destruct" expects either a disjunctiveHugo Herbelin
2014-11-07Test for #3542 fixed some time ago.Hugo Herbelin
2014-11-06Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Hugo Herbelin
2014-11-06Restoring clear_flag (thanks a lot to jonikelee to notice it).Hugo Herbelin
2014-11-06Optimizing when to clear generalized hypotheses in destruct.Hugo Herbelin
2014-11-06Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.Hugo Herbelin
2014-11-06Removing "destruct" test not yet working.Hugo Herbelin
2014-11-04test suite: some reproduction cases for recently-reported bugs.Xavier Clerc
2014-11-04Test for bug #2149.Pierre-Marie Pédrot
2014-11-03New bugs revealed fixed: #3408 by (probably) Maxime's commitsHugo Herbelin
2014-11-03Subtle swap of lines to preserve VarInstance src field before checkingHugo Herbelin
2014-11-03Fix to 844431761 on improving elimination with indices, getting rid ofHugo Herbelin
2014-11-02Improving elimination with indices, getting rid of intrusive residualHugo Herbelin
2014-11-02Some reorganization of the code for destruct/induction:Hugo Herbelin
2014-11-02Fixing file destruct.v.Hugo Herbelin
2014-10-31Enlarge the cases where the like first selection is used in destruct.Hugo Herbelin
2014-10-31Listing a few examples of destruct showing unsatisfactory behaviors.Hugo Herbelin
2014-10-31Avoid "destruct H" to apply on H itself when H is a section variable.Hugo Herbelin
2014-10-27Making destruct on idents with maximal implicit arguments working, byHugo Herbelin
2014-10-27Ensuring compatibility when an hypothesis used for destruct isHugo Herbelin
2014-10-27Fixing clash in test destruct.v.Hugo Herbelin