diff options
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 9ef6e317..33b570b9 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -85,8 +85,6 @@ Inductive wt_instr : instruction -> Prop := tailcall_possible sig -> match ros with inl r => r = IT1 | _ => True end -> wt_instr (Ltailcall sig ros) - | wt_Lalloc: - wt_instr Lalloc | wt_Llabel: forall lbl, wt_instr (Llabel lbl) |