diff options
| author | Guillaume Melquiond | 2020-08-30 10:35:45 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-11-13 15:13:23 +0100 |
| commit | 2d3e012cce7ca41893d670196d3c90e7e315403e (patch) | |
| tree | 7e9be9def2269bfffd55c3dff1a92127c47ac47f /kernel/vmbytegen.ml | |
| parent | 203211090f9e67750a0f953d6dbefe5045271921 (diff) | |
Remove unused if-then-else construct from VM.
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 |