From 842190a7a7c85b15f663fdf299a1f015a774f416 Mon Sep 17 00:00:00 2001 From: xleroy 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/SimplExprproof.v | 14 -------------- 1 file changed, 14 deletions(-) (limited to 'cfrontend/SimplExprproof.v') diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 9134e11e..0a77b191 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -105,19 +105,6 @@ Proof. intros. inv H; auto. Qed. -Lemma type_of_global_preserved: - forall b ty, - Csem.type_of_global ge b = Some ty -> - type_of_global tge b = Some ty. -Proof. - intros until ty. unfold Csem.type_of_global, type_of_global. - rewrite varinfo_preserved. destruct (Genv.find_var_info ge b). auto. - case_eq (Genv.find_funct_ptr ge b); intros. - inv H0. exploit function_ptr_translated; eauto. intros [tf [A B]]. - rewrite A. decEq. apply type_of_fundef_preserved; auto. - congruence. -Qed. - (** Translation of simple expressions. *) Lemma tr_simple_nil: @@ -269,7 +256,6 @@ Opaque makeif. (* var global *) split; auto. split; auto. apply eval_Evar_global; auto. rewrite symbols_preserved; auto. - eapply type_of_global_preserved; eauto. (* deref *) exploit H0; eauto. intros [A [B C]]. subst sl1. split; auto. split; auto. constructor; auto. -- cgit