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.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index 84de8f270..5ecc8d99c 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