From 00a63b73f267ae90cc868f14ab4f36db8185b3e0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 2 Mar 2018 21:46:55 +0100
Subject: [VM] Inject structured constants in values without reallocating them.

---
 kernel/cemitcodes.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'kernel/cemitcodes.ml')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index d4e35efa78..50f5607e31 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -358,10 +358,9 @@ let rec emit env insns remaining = match insns with
 type to_patch = emitcodes * patches * fv
 
 (* Substitution *)
-let rec subst_strcst s sc =
+let subst_strcst s sc =
   match sc with
-  | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc
-  | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
+  | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ -> sc
   | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
 
 let subst_reloc s ri =
-- 
cgit v1.2.3