diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /kernel/vmlambda.ml | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
Change the representation of kernel case.
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
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 |