aboutsummaryrefslogtreecommitdiff
path: root/pretyping/inferCumulativity.mli
AgeCommit message (Expand)Author
2019-09-25Move cumulativity inference to the kernel.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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