aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmvalues.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-02-04Primitive integersMaxime Dénès
2018-09-17OCaml now exports the min and max non-constant tags, let's use itMaxime Dénès
2018-09-17[VM] Inject structured constants in values without reallocating them.Maxime Dénès
2018-09-17[VM] Move structured_constant to VmvaluesMaxime Dénès
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-10[VM] Remove projection names from structured constants.Maxime Dénès
2018-03-26Moving the VM global atom table to a ML reference.Pierre-Marie Pédrot
2018-03-26Moving the VM global data to a ML reference.Pierre-Marie Pédrot
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-03Handling evars in the VM.Pierre-Marie Pédrot
2018-03-02[VM] Unify Const_sorts and Const_type, and remove Vsort.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-01-26Safer VM interfacesMaxime Dénès