From 6f9b68c8de22fe540bfe85c2fabec4b967c6a80d Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:58:24 +0000 Subject: Removed useless constraints on return type at Sreturn instructions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index e28228ab..5b2ad9b5 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -2965,7 +2965,7 @@ Proof. eapply external_call_nextblock_incr; eauto. eapply external_call_nextblock_incr; eauto. -(* return none *) +(* return *) inv MK. simpl. left; econstructor; split. apply plus_one. econstructor; eauto. -- cgit