diff options
Diffstat (limited to 'kernel/vmlambda.ml')
| -rw-r--r-- | kernel/vmlambda.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index 390fa58883..91de58b0e6 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -674,7 +674,8 @@ let rec lambda_of_constr env c = | Construct _ -> lambda_of_app env c empty_args - | 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.global_env (ci, u, pms, t, iv, a, br) in let ind = ci.ci_ind in let mib = lookup_mind (fst ind) env.global_env in let oib = mib.mind_packets.(snd ind) in |