diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-20 09:52:30 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-20 09:52:30 +0000 |
| commit | 842190a7a7c85b15f663fdf299a1f015a774f416 (patch) | |
| tree | 70c467bf21255737f3b28b10972478896599c740 /cfrontend/SimplExprproof.v | |
| parent | 3ec022950ec233a2af418aacd1755fce4d701724 (diff) | |
| download | compcert-kvx-842190a7a7c85b15f663fdf299a1f015a774f416.tar.gz compcert-kvx-842190a7a7c85b15f663fdf299a1f015a774f416.zip | |
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
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 14 |
1 files changed, 0 insertions, 14 deletions
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. |