aboutsummaryrefslogtreecommitdiff
path: root/pretyping/heads.ml
AgeCommit message (Expand)Author
2019-04-10Remove calls to Global.env in HeadsMaxime Dénès
2019-04-05Remove cache in HeadsMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-16Heads: simplify using that projections are always rigidGaëtan Gilbert
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-24Move Heads to pretyping (is_projection will move to Recordops)Gaëtan Gilbert