From 842190a7a7c85b15f663fdf299a1f015a774f416 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 20 Feb 2014 09:52:30 +0000
Subject: Remove useless checks on type_of_global in dynamic semantics

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2411 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Csem.v | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'cfrontend/Csem.v')

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 2eedbd8..5acf23f 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -189,19 +189,6 @@ Section SEMANTICS.
 
 Variable ge: genv.
 
-(** [type_of_global b] returns the type of the global variable or function
-  at address [b]. *)
-
-Definition type_of_global (b: block) : option type :=
-  match Genv.find_var_info ge b with
-  | Some gv => Some gv.(gvar_info)
-  | None =>
-      match Genv.find_funct_ptr ge b with
-      | Some fd => Some(type_of_fundef fd)
-      | None => None
-      end
-  end.
-
 (** ** Reduction semantics for expressions *)
 
 Section EXPR.
@@ -223,7 +210,6 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop :=
   | red_var_global: forall x ty m b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
-      type_of_global b = Some ty ->
       lred (Evar x ty) m
            (Eloc b Int.zero ty) m
   | red_deref: forall b ofs ty1 ty m,
-- 
cgit v1.2.3