aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2014-10-26Fixing destruct/induction with a using clause on a non-inductive type,Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-23Fixing clash in output test-suite Cases.Hugo Herbelin
2014-10-23Taking into account factorization of consecutive names of same typesHugo Herbelin
2014-10-22Fixing typo in output test Notations.Hugo Herbelin
2014-10-22Fix test-suite for #2729.Maxime Dénès
2014-10-22Fixing an evar leak in pattern-matching compilation (#3758).Hugo Herbelin
2014-10-21Adapting output tests to the removal of the new token warning and toHugo Herbelin
2014-10-21More precise test for #3459.Hugo Herbelin
2014-10-20Fixing a (new) part of bug #2729.Hugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-20Fixing a bug in the presence of let-in in inductive arity.Hugo Herbelin
2014-10-16Relaxing again the test on types of replacements in tactic changeHugo Herbelin
2014-10-16Fix test-suite scripts.Matthieu Sozeau
2014-10-16Bug fixed by Hugo.Matthieu Sozeau
2014-10-15Adding a timeout to bug #2447.Pierre-Marie Pédrot
2014-10-15To stay closer to non-primitive projections, only unfold primitiveMatthieu Sozeau
2014-10-15Fix for bug #3618.Matthieu Sozeau
2014-10-15Closed bug 3710.Matthieu Sozeau
2014-10-15Bug 3692 is fixed.Matthieu Sozeau
2014-10-15Bug 3628 is fixed.Matthieu Sozeau
2014-10-15Fix test-suite files which failed due to usage of $(admit)$ whichMatthieu Sozeau
2014-10-15Fix bug 3637.Matthieu Sozeau
2014-10-15Reenable FO unification of primitive projections and their eta-expandedMatthieu Sozeau
2014-10-15Fix test-suite file after moving back to using C as the nameMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 13:52:44 +0000