aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/cumulativity.v
AgeCommit message (Expand)Author
2017-07-31Change the option for cumulativityAmin Timany
2017-07-31Add Jason's example of fun-ext with cumulativityAmin Timany
2017-07-31Add test for NonCumulative inductivesAmin Timany
2017-07-31Issue error on monomorphic cumulative inductivesAmin Timany
2017-06-16Fix a bug in cumulativityAmin Timany
2017-06-16Move (part of) tests from checker to successAmin Timany