diff options
Diffstat (limited to 'backend/LTLintyping.v')
| -rw-r--r-- | backend/LTLintyping.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 26ec066d..9f3f5896 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -67,11 +67,6 @@ Inductive wt_instr : instruction -> Prop := sig.(sig_res) = funsig.(sig_res) -> Conventions.tailcall_possible sig -> wt_instr (Ltailcall sig ros args) - | wt_Lalloc: - forall arg res, - Loc.type arg = Tint -> Loc.type res = Tint -> - loc_acceptable arg -> loc_acceptable res -> - wt_instr (Lalloc arg res) | wt_Llabel: forall lbl, wt_instr (Llabel lbl) | wt_Lgoto: forall lbl, |