aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2014-10-15Implement a different strategy to expand primitive projections only whenMatthieu Sozeau
2014-10-14Fix bug #3698: stack overflow due to eta+canonical structures inMatthieu Sozeau
2014-10-13Added support for several impossible cases in compilation of "match".Hugo Herbelin
2014-10-08Fixing the anomaly in bug #3045 (a filter was not type-safe inHugo Herbelin
2014-10-07Add test-suite file for the projection unfolding bug I just fixed.Matthieu Sozeau
2014-10-07Fix test-suite file 3352 which was containing the wrong test.Matthieu Sozeau
2014-10-07Fix test-suite file to test original bug, not the failure of the guardMatthieu Sozeau
2014-10-05A few improvements on pattern-matching compilation.Hugo Herbelin
2014-10-03Classify segfaults as failures in opened bugs.Xavier Clerc
2014-10-03Classify segfaults as failures in opened bugsXavier Clerc
2014-10-03Fixing #3657 (check that both sides of a "change with" have the sameHugo Herbelin
2014-10-03Test for bug #3652 fixed in 0fb36157b9baHugo Herbelin
2014-10-03Fixing #3623 (unbound evars in types in a call to "change with").Hugo Herbelin
2014-10-03Add a bunch of reproduction files for bugs.Xavier Clerc
2014-10-03Adapting output/Arguments_renaming continued.Hugo Herbelin
2014-10-02Implement module subtyping for polymorphic constants (errors onMatthieu Sozeau
2014-10-02Fixing bug #2810 (autounfold on local variable declared as hint but cleared).Hugo Herbelin
2014-10-02An evar name changed in output test.Hugo Herbelin
2014-10-02Adapting the output test Notations:Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 12:46:03 +0000