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/Selectionproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index c292b49c..175b025c 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -380,7 +380,7 @@ Proof. exists (Val.longofwords (Vint (Int64.hiword i)) (Vint (Int64.loword i))); split. eapply eval_Eop. constructor. EvalOp. simpl; eauto. constructor. EvalOp. simpl; eauto. constructor. auto. simpl. rewrite Int64.ofwords_recompose. auto. - rewrite <- symbols_preserved. fold (symbol_address tge i i0). apply eval_addrsymbol. + rewrite <- symbols_preserved. fold (Genv.symbol_address tge i i0). apply eval_addrsymbol. apply eval_addrstack. (* Eunop *) exploit IHeval_expr; eauto. intros [v1' [A B]]. -- cgit