From 675b23dcf824d8a851881171a5628b239aad2201 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 May 2020 13:58:23 +0200
Subject: Remove redundant data from VM case switch.

No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.

Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
---
 dev/vm_printers.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index aa650fbdc8..ac4972ed0d 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,6 +1,5 @@
 open Format
 open Term
-open Constr
 open Names
 open Cemitcodes
 open Vmvalues
@@ -8,9 +7,7 @@ open Vmvalues
 let ppripos (ri,pos) =
   (match ri with
   | Reloc_annot a ->
-      let sp,i = a.ci.ci_ind in
-      print_string
-        ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
+      print_string "switch\n"
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
-- 
cgit v1.2.3