From 42d91c271a176de5029c216ef74e913ac7dec2e1 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 14 Jan 2018 16:16:13 -0800 Subject: Safer VM interfaces We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays. --- kernel/kernel.mllib | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/kernel.mllib') diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 917e4f6f1..749854b8c 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -16,6 +16,7 @@ Cemitcodes Opaqueproof Declarations Entries +Vmvalues Nativevalues CPrimitives Declareops -- cgit v1.2.3