From f774d5f2d604f747e72e2d3bb56cc3f90090e2dd Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 15 Feb 2013 16:24:13 +0000
Subject: Pointers one past

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Inlining.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/Inlining.v')

diff --git a/backend/Inlining.v b/backend/Inlining.v
index 5075fd6f..a9b1e7ea 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -454,7 +454,7 @@ Local Open Scope string_scope.
 
 Definition transf_function (fenv: funenv) (f: function) : Errors.res function :=
   let '(R ctx s _) := expand_function fenv f initstate in
-  if zle s.(st_stksize) Int.max_unsigned then
+  if zlt s.(st_stksize) Int.max_unsigned then
     OK (mkfunction f.(fn_sig) 
                    (sregs ctx f.(fn_params))
                    s.(st_stksize)
-- 
cgit