From 375a47bab8395695a4f74e19691854d2d0248045 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 23 Feb 2018 23:28:44 +0100
Subject: [VM] Remove projection names from structured constants.

It was actually a hack since those names are never used to represent
values, only to be passed as arguments to bytecode instructions. So
instead of reusing the structured_constant type, we follow the same
pattern as switch annotations.
---
 kernel/vmvalues.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/vmvalues.ml')

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 7a703e6537..8524c44d21 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -297,7 +297,6 @@ let rec obj_of_str_const str =
   match str with
   | Const_sort s -> obj_of_atom (Asort s)
   | Const_ind ind -> obj_of_atom (Aind ind)
-  | Const_proj p -> Obj.repr p
   | Const_b0 tag -> Obj.repr tag
   | Const_bn(tag, args) ->
       let len = Array.length args in
@@ -355,6 +354,7 @@ let val_of_constant c = val_of_idkey (ConstKey c)
 let val_of_evar evk = val_of_idkey (EvarKey evk)
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
+external val_of_proj_name : Constant.t -> values = "%identity"
 
 (*************************************************)
 (** Operations manipulating data types ***********)
-- 
cgit v1.2.3