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/csymtable.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/csymtable.mli')

diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 91bb30e7ed..fc935f6ee9 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -12,7 +12,7 @@ open Names
 open Constr
 open Pre_env
 
-val val_of_constr : env -> constr -> values
+val val_of_constr : env -> constr -> Vmvalues.values
 
 val set_opaque_const      : Constant.t -> unit
 val set_transparent_const : Constant.t -> unit
-- 
cgit v1.2.3