aboutsummaryrefslogtreecommitdiff
path: root/pretyping/inferCumulativity.mli
AgeCommit message (Expand)Author
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert