aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/cumulativity.v
AgeCommit message (Expand)Author
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
2018-03-09Fix expected number of arguments for cumulative constructors.Gaëtan Gilbert
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-08Add test-suite file for cumulative constructorsMatthieu Sozeau
2018-02-16Cleaner treatment of parameters in inferCumulativityGaëtan Gilbert
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:39:58 +0000