From 3fa79790e617d87584598746296e626e0ce3b256 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 24 May 2014 09:46:07 +0000 Subject: Refactoring: move symbol_offset into Genv. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constpropproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index d88d6e43..ecae5dc6 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -133,7 +133,7 @@ Proof. destruct (areg ae r); auto. destruct p; auto. predSpec Int.eq Int.eq_spec ofs Int.zero; intros; auto. subst ofs. exploit vmatch_ptr_gl; eauto. intros LD'. inv LD'; try discriminate. - rewrite H1 in FF. unfold symbol_address in FF. + rewrite H1 in FF. unfold Genv.symbol_address in FF. simpl. rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|]; try discriminate. simpl in FF. rewrite dec_eq_true in FF. @@ -162,8 +162,8 @@ Proof. - (* pointer *) destruct p; try discriminate. + (* global *) - inv H. exists (symbol_address ge id ofs); split. - unfold symbol_address. rewrite <- symbols_preserved. reflexivity. + inv H. exists (Genv.symbol_address ge id ofs); split. + unfold Genv.symbol_address. rewrite <- symbols_preserved. reflexivity. eapply vmatch_ptr_gl; eauto. + (* stack *) inv H. exists (Vptr sp ofs); split. -- cgit