aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/cumulativity.v
Commit message (Expand)AuthorAge
* Fix expected number of arguments for cumulative constructors.Gravatar Gaëtan Gilbert2018-03-09
* Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Add test-suite file for cumulative constructorsGravatar Matthieu Sozeau2018-03-08
* Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
* Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* Change the option for cumulativityGravatar Amin Timany2017-07-31
* Add Jason's example of fun-ext with cumulativityGravatar Amin Timany2017-07-31
* Add test for NonCumulative inductivesGravatar Amin Timany2017-07-31
* Issue error on monomorphic cumulative inductivesGravatar Amin Timany2017-07-31
* Fix a bug in cumulativityGravatar Amin Timany2017-06-16
* Move (part of) tests from checker to successGravatar Amin Timany2017-06-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 07:14:43 +0000