aboutsummaryrefslogtreecommitdiff
path: root/kernel/indTyping.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
2020-03-08Do not hardcode specific handling of Prop levels in template poly.Pierre-Marie Pédrot
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-01-21Refactor typechecking of inductive typesGaëtan Gilbert
2019-01-21Move inductive typecheck to file independent from positivity check.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:00:09 +0000