From aaa49526068f528f2233de0dace43549432fba52 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 12 Apr 2008 12:55:21 +0000
Subject: Revu gestion retaddr et link dans Stacking

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/RTLtyping.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'backend/RTLtyping.v')

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index a30f9e50..fa9dd210 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -224,7 +224,7 @@ Definition check_instr (i: instruction) : bool :=
       match ros with inl r => check_reg r Tint | inr s => true end
       && check_regs args sig.(sig_args)
       && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res)
-      && zeq (Conventions.size_arguments sig) 14
+      && Conventions.tailcall_is_possible sig
   | Ialloc arg res s =>
       check_reg arg Tint 
       && check_reg res Tint
@@ -330,8 +330,7 @@ Proof.
   destruct s0; auto. apply check_reg_correct; auto.
   eapply proj_sumbool_true; eauto.
   apply check_regs_correct; auto.
-  rewrite Conventions.tailcall_possible_size. 
-  eapply proj_sumbool_true; eauto.
+  apply Conventions.tailcall_is_possible_correct; auto.
   (* alloc *)
   constructor. 
   apply check_reg_correct; auto.
-- 
cgit