From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 13 Jun 2011 18:11:19 +0000 Subject: Revised handling of annotation statements, and more generally built-in functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Reloadtyping.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'backend/Reloadtyping.v') diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 60be59b9..eba5ad62 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -33,9 +33,7 @@ Require Import Reloadproof. generate well-typed instruction sequences, given sufficient typing and well-formedness hypotheses over the locations involved. *) -Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove - wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lbuiltin - wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty. +Hint Constructors wt_instr: reloadty. Remark wt_code_cons: forall f i c, wt_instr f i -> wt_code f c -> wt_code f (i :: c). @@ -292,9 +290,12 @@ Proof. destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. auto 10 with reloadty. + destruct (ef_reloads ef) as [] _eqn. + assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence. assert (map mreg_type (regs_for args) = map Loc.type args). apply wt_regs_for. apply arity_ok_enough. congruence. assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty. + auto 10 with reloadty. auto with reloadty. -- cgit