From a51cce369b9c634a93120092d4c7685a242d55b1 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 4 Jul 2015 14:22:08 +0200 Subject: Fix handling of primitive projections in VM. I'm pushing this patch now because the previous treatment of such projections in the VM was already unsound. It should however be carefully reviewed. --- kernel/cbytecodes.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/cbytecodes.mli') diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index d9998c89e..745ef311b 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -25,6 +25,7 @@ val last_variant_tag : tag type structured_constant = | Const_sorts of sorts | Const_ind of pinductive + | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -72,6 +73,8 @@ type instruction = | Ksetfield of int | Kstop | Ksequence of bytecodes * bytecodes + | Kproj of int * Constant.t (** index of the projected argument, + name of projection *) (** spiwack: instructions concerning integers *) | Kbranch of Label.t (** jump to label, is it needed ? *) -- cgit v1.2.3