From bcc49e9df3e1885fcdf6e7a082f9101a323fb39c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 4 Jan 2009 16:00:07 +0000 Subject: Cminor, CminorSel: removed useless premises in rules for Sreturn git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@938 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Selectionproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/Selectionproof.v') diff --git a/arm/Selectionproof.v b/arm/Selectionproof.v index e487d15a..a307597a 100644 --- a/arm/Selectionproof.v +++ b/arm/Selectionproof.v @@ -1427,11 +1427,11 @@ Proof. constructor; auto. destruct b; auto. (* Sreturn None *) econstructor; split. - econstructor. rewrite <- H; reflexivity. + econstructor. constructor; auto. apply call_cont_commut. (* Sreturn Some *) econstructor; split. - econstructor. simpl. auto. eauto with evalexpr. + econstructor. simpl. eauto with evalexpr. constructor; auto. apply call_cont_commut. (* Sgoto *) econstructor; split. -- cgit