From 6f9b68c8de22fe540bfe85c2fabec4b967c6a80d Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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/Clight.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'cfrontend/Clight.v')

diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 4cc97ab2..4f4123e0 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -533,7 +533,6 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State f Sskip k e le m)
 
   | step_return_0: forall f k e le m m',
-      f.(fn_return) = Tvoid ->
       Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f (Sreturn None) k e le m)
         E0 (Returnstate Vundef (call_cont k) m')
-- 
cgit