diff options
Diffstat (limited to 'backend/Reloadtyping.v')
| -rw-r--r-- | backend/Reloadtyping.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index df0715ee..1bb462dc 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -34,7 +34,7 @@ Require Import Reloadproof. 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_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lbuiltin wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty. Remark wt_code_cons: @@ -292,6 +292,13 @@ Proof. auto 10 with reloadty. 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 with reloadty. + + + + assert (map mreg_type (regs_for args) = map Loc.type args). eauto with reloadty. auto with reloadty. |