aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqchk/inductive_functor_template.v
AgeCommit message (Expand)Author
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaƫtan Gilbert