diff options
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index b27c53ef0f..f3b483467d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -535,7 +535,8 @@ let rec lambda_of_constr cache env sigma c = let prefix = get_mind_prefix env (fst ind) in mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|] - | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *) + | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *) + let (ci, t, _iv, a, branches) = Inductive.expand_case env (ci, u, pms, t, iv, a, br) in let (mind,i as ind) = ci.ci_ind in let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in |