aboutsummaryrefslogtreecommitdiff
path: root/pretyping/heads.ml
AgeCommit message (Expand)Author
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