diff options
Diffstat (limited to 'kernel/vmbytegen.ml')
| -rw-r--r-- | kernel/vmbytegen.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 489929d2be..5f6d19884f 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -657,18 +657,6 @@ let rec compile_lam env cenv lam sz cont = compile_fv cenv fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) - | Lif(t, bt, bf) -> - let branch, cont = make_branch cont in - let lbl_true = Label.create() in - let lbl_false = Label.create() in - compile_lam env cenv t sz - (Kswitch([|lbl_true;lbl_false|],[||]) :: - Klabel lbl_false :: - compile_lam env cenv bf sz - (branch :: - Klabel lbl_true :: - compile_lam env cenv bt sz cont)) - | Lcase(ci,rtbl,t,a,branches) -> let ind = ci.ci_ind in let mib = lookup_mind (fst ind) env in |