From 600e73d2522599fd600ab717410254565d57236b Mon Sep 17 00:00:00 2001
From: glondu
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/csymtable.ml | 2 +-
 kernel/vm.ml        | 2 ++
 kernel/vm.mli       | 2 ++
 3 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 58a5bf3278..145ca27d2e 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -102,7 +102,7 @@ let slot_for_str_cst key =
 let slot_for_annot key =
   try Hashtbl.find annot_tbl key
   with Not_found ->
-    let n =  set_global (Obj.magic key) in
+    let n =  set_global (val_of_annot_switch key) in
     Hashtbl.add annot_tbl key n;
     n
 
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 59681e8f1f..338936250c 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))
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 84de8f270f..5ecc8d99c0 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -59,6 +59,8 @@ val val_of_named_def : identifier -> values -> values
 val val_of_constant : constant -> values
 val val_of_constant_def : int -> constant -> values -> values
 
+external val_of_annot_switch : annot_switch -> values = "%identity"
+
 (** Destructors *)
 val whd_val : values -> whd
 
-- 
cgit v1.2.3