aboutsummaryrefslogtreecommitdiff
path: root/kernel/indTyping.ml
AgeCommit message (Expand)Author
2019-01-21Refactor typechecking of inductive typesGaëtan Gilbert
2019-01-21Move inductive typecheck to file independent from positivity check.Gaëtan Gilbert