aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inferCumulativity.ml
Commit message (Expand)AuthorAge
* Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
* Fix reduction flags in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
* inferCumulativity: add comment to explain [if not is_arity].Gravatar Gaëtan Gilbert2018-02-11
* Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11