aboutsummaryrefslogtreecommitdiff
path: root/pretyping/heads.ml
AgeCommit message (Expand)Author
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-21Remove the artificial dependency of Heads on evaluable_global_reference.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-07-01[pretyping] Remove seemingly unless check about "variable" opacity.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:36:31 +0000