From 5157b587bea1dd41635961ba1b01f85c6917c88e Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 30 Aug 2013 12:20:05 +0000
Subject: Remove Obj.magic from safe typing

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

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5ff619ce15..7a25cc5f80 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -169,12 +169,8 @@ let check_engagement env c =
 
 (** {6 Stm machinery } *)
 
-(* type to be maintained isomorphic to Entries.side_effects *)
-(* XXX ideally this function obtains a valid side effect that 
- * can be pushed into another (safe) environment without re-typechecking *)
-type side_effect = NewConstant of constant * constant_body
-let sideff_of_con env c = 
-  Obj.magic (NewConstant (c, Environ.lookup_constant c env.env))
+type side_effect = Declarations.side_effect
+let sideff_of_con env c = NewConstant (c, Environ.lookup_constant c env.env)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
-- 
cgit v1.2.3