From f02e6260f1cf1f49121860cfd95b6adb97db48ee Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 1 Mar 2018 14:43:07 +0100
Subject: [VM] Move structured_constant to Vmvalues

---
 dev/vm_printers.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 98190b05b5..47cfeb98d7 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -2,7 +2,6 @@ open Format
 open Term
 open Constr
 open Names
-open Cbytecodes
 open Cemitcodes
 open Vmvalues
 
-- 
cgit v1.2.3