From c47b205206d832430fa80a3386be80149e281d33 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:04:56 +0200
Subject: Code cleaning in VM (with Benjamin).

Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
---
 dev/vm_printers.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev/vm_printers.ml')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 3d688011c2..802b0f9d80 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -61,7 +61,6 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Aiddef(idk,_) -> print_string "&";print_idkey idk
   | Aind((sp,i),_) ->  print_string "Ind(";
       print_string (string_of_mind sp);
       print_string ","; print_int i;
-- 
cgit v1.2.3