From 600e73d2522599fd600ab717410254565d57236b Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 13 Nov 2009 16:45:22 +0000
Subject: Move Obj.magic call to the Vm module

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12523 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/vm.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/vm.ml')

diff --git a/kernel/vm.ml b/kernel/vm.ml
index 59681e8f1..338936250 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -343,6 +343,8 @@ let val_of_constant_def n c v =
   Obj.set_field res 1 (Obj.repr (Aiddef(ConstKey c, v)));
   val_of_obj res
 
+external val_of_annot_switch : annot_switch -> values = "%identity"
+
 let mkrel_vstack k arity =
   let max = k + arity - 1 in
   Array.init arity (fun i -> val_of_rel (max - i))
-- 
cgit v1.2.3