diff options
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 7dc601fb..9ef6e317 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -83,7 +83,7 @@ Inductive wt_instr : instruction -> Prop := | wt_Ltailcall: forall sig ros, tailcall_possible sig -> - match ros with inl r => r = IT3 | _ => True end -> + match ros with inl r => r = IT1 | _ => True end -> wt_instr (Ltailcall sig ros) | wt_Lalloc: wt_instr Lalloc |